v8.4: Fixing buggy detection of disjunction-like inductive types (bug #2907).

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15917 85f007b7-540e-0410-9357-904b9bb8a0f7
Restore RefMan-tac.tex to state prior to commit 15554 (oups...)

 Sorry, probably something has gone wrong during a conflit resolution

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15918 85f007b7-540e-0410-9357-904b9bb8a0f7
Restore documentation of eqn:H

 Cf. commits 15568 and 15569

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15919 85f007b7-540e-0410-9357-904b9bb8a0f7
Text inserted by insert_this_phrase_on_success correct tagging

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15921 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqmktop: missing -I (fix #2851)

 The modules used in coqmktop's temporary main file should have
 their .cmi in the search path, hence a small set of -I is required:
 lib, toplevel. We do not place their the full list to avoid issues
 with the win32 command-line length

 Btw, coqmktop -boot now also builds its list of -I instead of receiving
 them via its command-line, it's simpler this way...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15927 85f007b7-540e-0410-9357-904b9bb8a0f7
 the new .dir-locals.el thanks to Pierre Courtieu

As it says :
Set default directory to coq root ONLY IF variable
coq-project-find-file is non nil. This should remain a
user preference and not be set by default. This setting
is redundant with compile-command above as M-x compile
always CD's to default directory. To enable it add this
to your emacs config: (setq coq-project-find-file t)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15933 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide for Gtk-mac-integration 2.0.0 (backport)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15934 85f007b7-540e-0410-9357-904b9bb8a0f7
Makefile: stop using ln -s in win32

In Win32, cygwin provides an emulation of ln -s, but this emulation
won't work outside of cygwin shell (i.e. typically in a Sys.command).
So we just forget about it, and do a simple copy.

This is just a workaround, the long-term solution is already in trunk:
do not produce coqtop.opt(.exe) anymore, but only coqtop(.exe).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15936 85f007b7-540e-0410-9357-904b9bb8a0f7
Allow running coq-tex in win32 (fix #2921)

 Yes, it seems that < and > and even 2>&1 are legal under windows :-)

 Btw, the only function using streams has been rewritten, so coq_tex
 is now a standard .ml file, not a .ml4 anymore (beware during upgrade!)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15937 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix Separate extraction when a module-as-file is aliased (#2917)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15941 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix Extraction Implicit on axioms.

There was a small bug causing the type in OCaml commentary not to honor
the implicit declaration, whereas the rest of the code did.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15944 85f007b7-540e-0410-9357-904b9bb8a0f7
Extraction Implicit: consider the parameters of a constructor (fix #2905)

 The parameters of a constructor C are part of the type of C,
 we should take them in account when retrieving the argument(s)
 declared as implicit.

 This way, the Extraction Implicit should now be correct when
 given named arguments of constructors with parameters.

 When positional numbers are given to Extraction Implicit, these
 numbers should now be increased by the number of parameters for
 this constructor.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15945 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide Detach View: avoid doing gtk stuff in sub-thread (fix #2863)

 In Win32, playing with gtk stuff outside gtk's main loop causes
 coqide to crash: we should be careful when using do_if_not_computing
 and its Thread.create. In the case of Detach View anyway, the
 do_if_not_computing was clearly useless. Strangely, the unix gtk
 seems more resilient and was not crashing ...

 Btw, avoid maintaining a thread-unsafe list of detached_views,
 use instead gtk callbacks to close detached views when their
 corresponding buffer in the main window is closed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15949 85f007b7-540e-0410-9357-904b9bb8a0f7
coqdep: honor dependencies of "Load"ed files

Imagine A.v "Load"s B.v and that B.v "Require"s C.
Before this commit we get:

  A.vo: A.v B.v

After this commit we get:

  A.vo: A.v B.v C.vo

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15951 85f007b7-540e-0410-9357-904b9bb8a0f7
Xml_parser: detect immediate EOF as a new error Xml_parser.Empty

 Without this immediate EOF detection, coqtop -ideslave loops
 when its input channel is closed.

 This is a partial backport of trunk commit 15959.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15963 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide : allow properly closing communication pipes with coqtop

 NB: it's important to close coqide's descriptors (ide2top_w and top2ide_r)
 in coqtop. We do this indirectly via [Unix.set_close_on_exec].
 This way, coqide has the only remaining copies of these descriptors,
 and closing them later will have visible effects in coqtop. Cf man 7 pipe
 for more details.

 This should avoid the need for Unix.kill on coqtop clients (at least
 when they aren't inside a long computation).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15964 85f007b7-540e-0410-9357-904b9bb8a0f7
coq_makefile: use coqdep instead of ocamldep on .ml4 files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15966 85f007b7-540e-0410-9357-904b9bb8a0f7
Updated .dir-locals.el (backport of r15974)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15982 85f007b7-540e-0410-9357-904b9bb8a0f7
Ide_intf.to_answer: dynamically check that answer & call correspond

 Without this, it was probably possible to crash Coqide by forging
 inadequate answers to a call. Backport of trunk commits 15983-15985.

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