Previous version did compile but did not make it possible to actually run

pcoq.  This version does work.

Main modification is:

- change centaur.ml4 so that
  * the Pcoq mode is really started by Start Pcoq Mode.
  * Reset <id> and Reset Initial work as planned for Pcoq (commands
    are Pcoq Reset <id> and Pcoq ResetInitial).
  * current_proof_name() does not raise an exception when there is no current
    proof.

- change xlate.ml so that the main tacticals are translated correctly to
  pcoq data structures.

- change in ascent.mli so that
  * we make sure Fail can now have a numeric argument,
  * progress is added

- vtp.ml is changed in accordance with ascent.mli


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

0 files changed, 0 insertions, 0 deletions