Coqmktop and camlp4 : sequel to commit 16113

 Actually I don't see any reason to link q_utils and q_coqast
 in coqtop.byte specifically when using camlp4 (and not camlp5).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16121 85f007b7-540e-0410-9357-904b9bb8a0f7
Envar: in w32, add .exe when searching for caml binaries

 Based on a patch by Pierre-Yves Strub

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

This reverts commit d14b9f6a017347e59cf037ff576f282785105080.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
Evarconv: Check stack before term in Canonical Structure approuval

3 days of work to swap 2 lines ... but this fixes LemmaOverloading
(and hopfully makes Feit-Thomson compilation time back to "normal")

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16130 85f007b7-540e-0410-9357-904b9bb8a0f7
I forget to use git log before git svn dcommit ...

Revert "Revert "coq_makefile: use coqdep instead of ocamldep on .ml4 files""

This reverts commit 7b9856f2eae3bd652d99864c9901f7c4af290323.

The reason for my private revert is that coqdep does not find the dependencies
of .ml4 files in AACTactics user-contrib correctly but it is a coqdep bug not
a coq_makefile one ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16131 85f007b7-540e-0410-9357-904b9bb8a0f7
Last test-suite not in Symmetric Patterns syntax

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16132 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix bug 2958: Inductive deep in in clause are impossible

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16133 85f007b7-540e-0410-9357-904b9bb8a0f7
- Fix evarconv so that we have complete eta-conversion:
  - In the maybeflex/rigid (lambda) case, try eta if the maybeflex doesn't
actually unfold (e.g. vars, or the transparent state says it's opaque).
  - In the flexible/rigid(lambda) case, try eta if miller-pfenning fails
(as the stack might not be a purely applicative one). This will zip the
flexible term (a case construct most likely) and try eta expansion on it.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16134 85f007b7-540e-0410-9357-904b9bb8a0f7
Revert "remove -rectypes except for term.ml"

Preparing landing of the native compiler, which requires -rectypes flag.

This reverts commit f975575187d0a19e7cc1afc43459a92eeb12b3f1.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16135 85f007b7-540e-0410-9357-904b9bb8a0f7
New implementation of the conversion test, using normalization by evaluation to
native OCaml code.

Warning: the "retroknowledge" mechanism has not been ported to the native
compiler, because integers and persistent arrays will ultimately be defined as
primitive constructions. Until then, computation on numbers may be faster using
the VM, since it takes advantage of machine integers.



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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16137 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide: avoid potentially blocking read on coqtop channel

 With Pierre-Marie, we discovered the hard way that Glib.Io reads
 are *not* non-blocking by default as I thought. My bad...
 This was causing nasty freezes of coqide in the rare cases where
 the final read was exactly filling the buffer (which was of size 1024).

 Now:
 - the input channels from coqtop (and various other external commands)
   are given to Unix.set_nonblock
 - Exceptions in our io_read_all (typically a kind of EAGAIN) terminate
   the read
 - We can now switch to Glib.Io.read_chars instead of the deprecated
   Glib.Io.read.
 - Btw, we use a larger buffer (8192).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16138 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide: limit read buffer size to 4096 (pipe size in win32)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16139 85f007b7-540e-0410-9357-904b9bb8a0f7
Native compiler: warnings were not turned off for OCaml 3.11


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16140 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixed parsing of -no-native-compiler flag.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16141 85f007b7-540e-0410-9357-904b9bb8a0f7
Reductionops: whd_state_gen can take and answers a cst_stack too

+ cst_stack is kept en a meta/evar is "unfold".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16142 85f007b7-540e-0410-9357-904b9bb8a0f7
Hugo request: CoqIDE find on enter

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

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

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