Coqide for Gtk-mac-integration 2.0.0

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15922 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/trunk@15923 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/trunk@15924 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/trunk@15926 85f007b7-540e-0410-9357-904b9bb8a0f7
Cleared a purely declarative .ml file and moved its interface to intf/

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15928 85f007b7-540e-0410-9357-904b9bb8a0f7
Removed a few calls to "Opaque" in Logic.v ineffective since at least
V7.1. Thanks to Assia for reporting.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15929 85f007b7-540e-0410-9357-904b9bb8a0f7
Change Hint Resolve, Immediate to take a global reference as argument
instead of a general constr: this is the most common case and does
not loose generality (one can simply define constrs before Hint Resolving
them). Benefits:
- Natural semantics for typeclasses, not class resolution needed at
Hint Resolve time, meaning less trouble for users as well.
- Ability to [Hint Remove] any hint so declared.
- Simplifies the implementation as well.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15930 85f007b7-540e-0410-9357-904b9bb8a0f7
Moved Entries module back to kernel

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15931 85f007b7-540e-0410-9357-904b9bb8a0f7
Removed many calls to OCaml generic equality. This was done by
writing our own comparison functions, and enforcing monomorphization
in many places. This should be more efficient, btw. Still a work
in progress.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15932 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixed #2926:

Extend "Print Opaque Dependencies" for transparent dependencies as
well

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15935 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/trunk@15938 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/trunk@15939 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/trunk@15940 85f007b7-540e-0410-9357-904b9bb8a0f7
Extraction: avoid initial strange empty comments after Arnaud's hack

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15942 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/trunk@15943 85f007b7-540e-0410-9357-904b9bb8a0f7
Documenting the 'Printing Transparent/All Dependencies' command.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15946 85f007b7-540e-0410-9357-904b9bb8a0f7