Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)

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

2 files changed, 13 insertions, 9 deletions

diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index e6f6891f73..ffcb7c648e 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -52,7 +52,7 @@ let tuple_n n =
       (fun i -> 
 	 let id = id_of_string 
 		    ("proj_" ^ string_of_int n ^ "_" ^ string_of_int i) in
-	 (false, (id, true, Ast.nvar (id_of_string ("T" ^ string_of_int i)))))
+	 (false, Vernacexpr.AssumExpr (id, Ast.nvar (id_of_string ("T" ^ string_of_int i)))))
       l1n 
   in
   let cons = id_of_string ("Build_tuple_" ^ string_of_int n) in
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index c7f1fc2ed7..d191b58ebf 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -220,6 +220,14 @@ let reduce_open_constr (em0,c) =
   let em = existential_map_of_constr c in
   (em,c)
 
+let register id n =
+  let id' = match n with None -> id | Some id' -> id' in
+  Penv.register id id'
+
+let correctness_hook _ ref = 
+  let pf_id = Nameops.basename (Nametab.sp_of_global (Global.env()) ref) in
+  register pf_id None
+
 let correctness s p opttac =
   Pmisc.reset_names();
   let p,oc,cty,v = coqast_of_prog p in
@@ -228,14 +236,14 @@ let correctness s p opttac =
   let sigma = Evd.empty in
   let cty = Reduction.nf_betaiota cty in
   let id = id_of_string s in 
-  start_proof id Declare.NeverDischarge sign cty;
+  start_proof id (false,Nametab.NeverDischarge) sign cty correctness_hook;
   Penv.new_edited id (v,p);
   if !debug then show_open_subgoals();
   deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ());
   let oc = reduce_open_constr oc in
   deb_mess (str"AFTER REDUCTION:" ++ fnl ());
   deb_mess (Printer.prterm_env (Global.env()) (snd oc));
-  let tac = (tclTHEN (Refine.refine_tac oc) automatic) in
+  let tac = (tclTHEN (Extratactics.refine_tac oc) automatic) in
   let tac = match opttac with 
     | None -> tac
     | Some t -> tclTHEN tac t
@@ -245,15 +253,11 @@ let correctness s p opttac =
 
 
 (* On redéfinit la commande "Save" pour enregistrer les nouveaux programmes *)
-
+(*
 open Vernacinterp
 
 let add = Vernacinterp.overwriting_vinterp_add
 
-let register id n =
-  let id' = match n with None -> id | Some id' -> id' in
-  Penv.register id id'
-
 let _ = 
   let current_save = Vernacinterp.vinterp_map "SaveNamed" in
   add "SaveNamed"
@@ -282,4 +286,4 @@ let _ =
 	let pf_id = Pfedit.get_current_proof_name () in
 	current_saveanonymous l ();
 	register pf_id (Some id)))
-
+*)