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

1 files changed, 31 insertions, 24 deletions

diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index a0620d4ba..b1602655f 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -57,7 +57,11 @@ let text_proof_flag = ref "en";;
 (* 
 let current_proof_name = ref "";;
 *)
-let current_proof_name () = string_of_id (get_current_proof_name ())
+let current_proof_name () = 
+  try 
+    string_of_id (get_current_proof_name ())
+  with
+      UserError("Pfedit.get_proof", _) -> "";;
 
 let current_goal_index = ref 0;;
 
@@ -482,6 +486,19 @@ let kill_node_verbose n =
 
 let set_text_mode s = text_proof_flag := s
 
+let pcoq_reset_initial() =
+  output_results(ctf_AbortedAllMessage()) None;
+  Vernacentries.abort_refine Lib.reset_initial ();
+  output_results(ctf_ResetInitialMessage()) None;;
+
+let pcoq_reset x =
+  if refining() then
+    output_results (ctf_AbortedAllMessage ()) None;
+    Vernacentries.abort_refine Lib.reset_name x;
+    output_results
+         (ctf_ResetIdentMessage !global_request_id (string_of_id x)) None;;
+
+
 VERNAC ARGUMENT EXTEND text_mode
 | [ "fr" ] -> [ "fr" ]
 | [ "en" ] -> [ "en" ]
@@ -512,6 +529,14 @@ VERNAC COMMAND EXTEND KillSubProof
   [ "Kill" "SubProof" natural(n) ] -> [ logical_kill n ]
 END
 
+VERNAC COMMAND EXTEND PcoqReset
+  [ "Pcoq" "Reset" ident(x) ] -> [ pcoq_reset x ]
+END
+
+VERNAC COMMAND EXTEND PcoqResetInitial
+  [ "Pcoq" "ResetInitial" ] -> [ pcoq_reset_initial() ]
+END
+
 let start_proof_hook () =
   History.start_proof (current_proof_name());
   current_goal_index := 1
@@ -909,38 +934,20 @@ let start_pcoq_mode debug =
     set_pcoq_hook pcoq_hook;
   end;;
 
-(*
-vinterp_add "START_PCOQ"
-            (function _ -> 
-              (function () ->
-                start_pcoq_mode false;
-		set_acknowledge_command ctf_acknowledge_command;
-                set_start_marker "CENTAUR_RESERVED_TOKEN_start_command";
-                set_end_marker "CENTAUR_RESERVED_TOKEN_end_command";
-                raise Vernacinterp.ProtectedLoop));;
-
-vinterp_add "START_PCOQ_DEBUG"
-            (function _ -> 
-              (function () ->
-                start_pcoq_mode true;
-		set_acknowledge_command ctf_acknowledge_command;
-                set_start_marker "--->";
-                set_end_marker "<---";
-                raise Vernacinterp.ProtectedLoop));;
-*)
+
 let start_pcoq () =
   start_pcoq_mode false;
   set_acknowledge_command ctf_acknowledge_command;
   set_start_marker "CENTAUR_RESERVED_TOKEN_start_command";
-  set_end_marker "CENTAUR_RESERVED_TOKEN_end_command"(*;
-  raise Vernacexpr.ProtectedLoop*)
+  set_end_marker "CENTAUR_RESERVED_TOKEN_end_command";
+  raise Vernacexpr.ProtectedLoop;;
 
 let start_pcoq_debug () =
   start_pcoq_mode true;
   set_acknowledge_command ctf_acknowledge_command;
   set_start_marker "--->";
-  set_end_marker "<---"(*;
-  raise Vernacexpr.ProtectedLoop;;*)
+  set_end_marker "<---";
+  raise Vernacexpr.ProtectedLoop;;
 
 VERNAC COMMAND EXTEND StartPcoq
   [ "Start" "Pcoq" "Mode" ] -> [ start_pcoq () ]