Coq_makefile : bug when a project file is not in the current directory.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14443 85f007b7-540e-0410-9357-904b9bb8a0f7
Automatic search of project file

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14444 85f007b7-540e-0410-9357-904b9bb8a0f7
Coq_makefile: bugfix in install rule

Files in a -I path are now installed in every root directory of -R pathes.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14445 85f007b7-540e-0410-9357-904b9bb8a0f7
Bug 2589: Documentation patch of Hendrik Tews

+ s/cbv/lazy of bug 2542

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14446 85f007b7-540e-0410-9357-904b9bb8a0f7
Bug 3596: ocamlbuild: coq_makefile now requires Unix

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14447 85f007b7-540e-0410-9357-904b9bb8a0f7
Having added a special Cast for remembering the use of conversion
tactic steps (r14407) increased the size of proof-terms, leading in
some cases (e.g. in Nijmegen/Algebra) to calls to simpl becoming
extremely costly on such terms built with tactics.

We try as a workaround to remove the newly introduced Cast after it
has been used by the type-checking algorithm.

We incidentally fixed eq_constr which was not fully transparent wrt
casts. We also removed useless code in judge_of_apply (has_revert).

Note: checker still to be updated to reflect a possible use of this
new kind of cast.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14448 85f007b7-540e-0410-9357-904b9bb8a0f7
Extraction Implicit: fix the numbering of constructor arguments

 For constructors, the numbers of parameters used to be wrongly
 ignored. Consider for instance :

  Inductive listn (A:Type) : nat -> Type :=
   | niln : listn A 0
   | consn : forall n, A -> listn A n -> listn A (S n).

 Saying "Extraction Implicit consn [n]" should now work correctly,
 and correspond to the alternative syntax "Extraction Implicit consn [2]",
 where 2 is the position of the argument n when counting with
 inductive parameters.

 Note that saying "Extraction Implicit consn [1]" (or [A]) is now
 a no-op : constructors have always been cleaned-up from their
 parameters during extraction.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14449 85f007b7-540e-0410-9357-904b9bb8a0f7
Util.error now creates UserError(_,msg) instead of UserError(str,str)

 This only affects display of errors when flag -debug is used,
 and it avoids strange message like "Error: in msg: msg"

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14450 85f007b7-540e-0410-9357-904b9bb8a0f7
Remove code concerning the obsolete Set/Unset Undo

 Even if they are no-ops now, the commands Set/Unset Undo themselves
 are kept for compatibility, in particular to avoid error messages
 or warnings during the initialization of ProofGeneral.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14451 85f007b7-540e-0410-9357-904b9bb8a0f7
Lib.node: merge OpenedModtype and OpenedModule, same for Closed...

 This allows more sharing of code (cf. start_module / end_module)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14452 85f007b7-540e-0410-9357-904b9bb8a0f7
Lib: remove strange code about backtracking to the current state

 We now forbid a "BackTo n" or "Backtrack n _ _" when n is
 the current label or a future one.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14453 85f007b7-540e-0410-9357-904b9bb8a0f7
Ide_intf: slight reorganisation of the IDE api

 - merge raw_interp with interp (with one more flag)
 - merge read_stdout with interp, which now return a string
 - shorter command names

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14454 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide: new backtracking code, based on the Backtrack command

 This approach, inspired by ProofGeneral, is *much* simplier than earlier,
 and should be more robust (I hope! feedback of testers is welcome).

 Coqide still continues to send orders like "Rewind 5" for undoing 5 phrases.
 A stack on the coqtop side (in Ide_slave) convert this phrase count to
 labels in the sense of Backtrack, and to abort + depth informations
 concerning proofs.

 We avoid re-entering finished proofs during Rewind by some extra backtracking
 until before these proofs. The amount of extra backtracking is then answered
 by coqtop to coqide. Now:
  - for go_to_insert (the "goto" button), unlike PG, coqide replays
    the extra backtracked zone.
  - for undo_last_step (the "back" button), coqide now leaves the extra
    backtracked zone undone, just like PG. This happens typically when
    undoing a Qed, and this should be the only visible semantical change
    of this patch.

 Two points to check with Pierre C:
  - such a coqtop-side stack mapping labels to opened proofs might be
    interesting to PG, instead of passing lots of info via the prompt and
    computing stuff in emacs.
  - Unlike PG, we allow re-entering inside a module / section, while
    PG retracts to the start of it. Coqide seems to work fine this way, to
    check.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14455 85f007b7-540e-0410-9357-904b9bb8a0f7
fake_ide: a short program to mimic an ide talking to coqtop -ideslave

  This way, we can test each night that coqtop -ideslave handles
  correctly some specific sequences of API calls.
  For the moment, we add a few tests of the backtracking.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14457 85f007b7-540e-0410-9357-904b9bb8a0f7
ide/preferences.ml: apparently no `META in Gdk.Tags.modifier

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14458 85f007b7-540e-0410-9357-904b9bb8a0f7
Avoid registering λ and Π as keywords just for some private Local Notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14459 85f007b7-540e-0410-9357-904b9bb8a0f7
test-suite/ide: misc improvement

 - make clean really erases *.log
 - some missing \n at end of files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14460 85f007b7-540e-0410-9357-904b9bb8a0f7
Improved ltac code for zify (fix #2575).

 Note nonetheless that the underlying bug is still active (cf. #2602),
 I've just written the ltac stuff in a nicer way (no nested match goal),
 and things happen to work now :-)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14461 85f007b7-540e-0410-9357-904b9bb8a0f7
make world now builds fake_ide (to please coq-bench)

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