Pfedit: avoid Undoing too much

 It seems that we can currently do a successful Undo (but not two!)
 on a freshly started Lemma. Let's add a depth check on Pfedit.undo
 to avoid that. This way, we cannot Undo to depth < 1 (with 1 being
 the initial depth of a lemma).

 Simplier implementation of Pfedit.restart : it is Pfedit.undo_todepth 1.

 This extra initial step in the Undo Stack has probably something
 to see with the Lemma argument introduction. For instance, before this
 patch we had:

 Lemma test n : n+0=n.
 Restart. (* now the goal is universally quantified ! *)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15132 85f007b7-540e-0410-9357-904b9bb8a0f7
Ppvernac: nicer printing of proof delimiters { ... }

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15133 85f007b7-540e-0410-9357-904b9bb8a0f7
Remove old proof-managment commands Suspend/Resume

There're not compatible with the current Backtrack mecanism used
both by ProofGeneral and CoqIDE.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15134 85f007b7-540e-0410-9357-904b9bb8a0f7
Remove undocumented command "Delete foo"

 This command isn't trivial to port to the forthcoming evolution of
 backtracking in coqtop. Moreover, it isn't clear whether this
 "Delete" works well in advanced situation (was not updating
 frozen states).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15135 85f007b7-540e-0410-9357-904b9bb8a0f7
A unified backtrack mechanism, with a basic "Show Script" as side-effect

 Migrate the backtracking code from ide_slave.ml into a new backtrack.ml.
 In particular the history stack of commands that used to be there is now
 non-coqide-specific.

 ** Adapted commands **

 - "Show Script": a basic functional version is restored (and the printing
 of scripts at Qed in coqtop). No indentation, one Coq command per line,
 based on the vernac_expr asts recorded in the history stack, printed via
 Ppvernac.

 - "Back n" : now mimics the backtrack of coqide: it goes n steps back
 (both commands and proofs), and maybe more if needed to avoid re-entering
 a proof (it outputs a warning in this case).

 - "BackTo n" : still try to go back to state n, but it also handles the
 proof state, and it may end on some state n' <= n if needed to avoid
 re-entering a proof. Ideally, it could someday be used by ProofGeneral
 instead of the complex Backtrack command.

 ** Compatible commands **

 - "Backtrack" is left intact from compatibility with current ProofGeneral.
 We simply re-synchronize the command history stack after each Backtrack.

 - "Undo" is kept as a standard command, not a backtracking one, a bit like
 "Focus". Same for "Restart" and "Abort". All of these are now accepted
 in coqide (Undo simply triggers a warning).

 - Undocumented command "Undo To n" (counting from start of proof instead of
 from end) also keep its semantics, it is simply made compatible with
 the new stack mechanism.

 ** New restrictions **

 We now forbid backtracking commands (Reset* / Back*) inside files
 when Load'ing or compiling, or inside VernacList/VernacTime/VernacFail.
 Too much work dealing with these situation that nobody uses.

 ** Internal details **

 Internally, the command stack differs a bit from what was in Ide_slave
 earlier (which was inspired by lisp code in ProofGeneral). We now tag
 commands that are unreachable by a backtrack, due to some proof being
 finished, aborted, restarted, or partly Undo'ed. This induce a bit of
 bookkeeping during Qed/Abort/Restart/Undo, but then the backtracking code
 is straightforward: we simply search backward the first reachable state
 starting from the desired place. We don't depend anymore on the proof
 names (apart in the last proof block), It's more robust this way
 (think of re-entering a M.foo from an outside proof foo).

 Many internal clarifications in Lib, Vernac, etc. For instance
 "Reset Initial" is now just a BackTo 1, while "Reset foo" now calls
 (Lib.label_before_name "foo"), and performs a BackTo to the corresponding
 label.

 Concerning Coqide, we directly suppress the regular printing of goals
 via a flag in Vernacentries. This avoid relying on a classification
 of commands in Ide_slave as earlier.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15136 85f007b7-540e-0410-9357-904b9bb8a0f7
Documentation of last commit concerning Backtracking

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15137 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix the test-suite by removing any Reset in the scripts

 Reset and the other backtracking commands (Back, BackTo, Backtrack)
 are now allowed only during interactive session, not in compiled
 or loaded scripts.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15138 85f007b7-540e-0410-9357-904b9bb8a0f7
Module names and constant/inductive names are now in two separate namespaces

 We now accept the following code: Definition E := 0. Module E. End E.

 Techically, we simply allow the same label to occur at most twice in
 a structure_body, which is a (label * structure_field_body) list).
 These two label occurences should not be at the same level of fields
 (e.g. a SFBmodule and a SFBmind are ok, but not two SFBmodule's or
 a SFBmodule and a SFBmodtype). Gain : a minimal amount of code change.
 Drawback : no more simple List.assoc or equivalent should be performed
 on a structure_body ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15139 85f007b7-540e-0410-9357-904b9bb8a0f7
Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconcl

 No grammar entries for these tactics since coq 8.0

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15140 85f007b7-540e-0410-9357-904b9bb8a0f7
info_trivial, info_auto, info_eauto, and debug (trivial|auto)

 To mitigate the lack of a general "info" tactical, let's
 introduce some specialized tactics info_trivial, info_auto
 and info_eauto that display the basic tactics used when
 solving a goal.

 We also add tactics "debug trivial" and "debug auto" which
 display every basic tactics attempted by trivial or auto.

 Triggering the "info" or "debug" mode for auto, eauto, trivial
 can also be done now via global options, such as Set Debug Auto
 or Set Info Eauto. In case both debug and info modes are
 activated, the debug mode takes precedence.

 NB: it would be nice to name these tactics "info xxx" instead
 of "info_xxx", but I don't see how to implement a "info eauto"
 in eauto.ml4 (hence by TACTIC EXTEND) while keeping
 a generic "info foo" tactic in g_ltac.ml4 (useful to display
 a nice message about the unavailability of the general info).

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

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

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