Move the examples about inversion to the chapters about tactics and schemes.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15262 85f007b7-540e-0410-9357-904b9bb8a0f7
A few improvements to the documentation about tactics.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15276 85f007b7-540e-0410-9357-904b9bb8a0f7
A few improvements to the documentation about tactics.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15277 85f007b7-540e-0410-9357-904b9bb8a0f7
A few improvements to the documentation about tactics.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15278 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4, Ref. man., ch. CIC: clarifying the redundancy coming from having both
Prop <= Type(i) and the conjunction of Prop <= Set and Set <= Type(i).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15285 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Rephrasing section on Sorts in CIC chapter, accordingly to discussions
with Assia and Guillaume.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15286 85f007b7-540e-0410-9357-904b9bb8a0f7
Documentation for Unfocused, braces and bullets.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15294 85f007b7-540e-0410-9357-904b9bb8a0f7
Addedum to documentation of bullets: I now use the dedicated coq_example
environment to display the example.


Conflicts:

	Makefile.common

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15296 85f007b7-540e-0410-9357-904b9bb8a0f7
Always add the Coq_config.dirs to xdg_dirs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15297 85f007b7-540e-0410-9357-904b9bb8a0f7
Tactic unfold always asks for comma between names.

Else the parser takes "at" as a constant to unfold in "unfold plus at ...".


Conflicts:

	parsing/g_tactic.ml4

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15298 85f007b7-540e-0410-9357-904b9bb8a0f7
Bug 2767

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15299 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide awful coqtop options parsing fixup

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15300 85f007b7-540e-0410-9357-904b9bb8a0f7
Backporting interface changes.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15304 85f007b7-540e-0410-9357-904b9bb8a0f7
Backporting the interface primitive to ask coqtop for its internal versions.

Conflicts:

	toplevel/ide_slave.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15305 85f007b7-540e-0410-9357-904b9bb8a0f7
Makefile.build typo in echo

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15309 85f007b7-540e-0410-9357-904b9bb8a0f7
Impossible branches inference fixup (bug 2761)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15310 85f007b7-540e-0410-9357-904b9bb8a0f7
Backported a SearchAbout-like primitive in coqtop interface.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15311 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide: display initial connection errors in popups instead of on stderr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15318 85f007b7-540e-0410-9357-904b9bb8a0f7
Makefile: Really avoid locales in $(DATE)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15319 85f007b7-540e-0410-9357-904b9bb8a0f7
when cross-compiling with mingw32, let's fix the Filename.dir_sep

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15320 85f007b7-540e-0410-9357-904b9bb8a0f7