nettoyage

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

3 files changed, 24 insertions, 46 deletions

diff --git a/contrib/correctness/pcicenv.ml b/contrib/correctness/pcicenv.ml
index eecc5eb2f..c1b4b0fa3 100644
--- a/contrib/correctness/pcicenv.ml
+++ b/contrib/correctness/pcicenv.ml
@@ -42,7 +42,7 @@ let set = mkCast (mkSet, mkType Univ.prop_univ)
  *)
 
 let cci_sign_of ren env =
-   Penv.fold_all 
+  Penv.fold_all 
     (fun (id,v) sign ->
        match v with
 	 | Penv.TypeV (Ref _ | Array _) -> sign
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index a91bceb8e..e9bb7c88f 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -140,7 +140,11 @@ let ast_zwf_zero loc =
 
 (* program -> Coq AST *)
 
-let bdize = Termast.ast_of_constr true (Global.env ())
+let bdize c = 
+  let env = 
+    Global.env_of_context (Pcicenv.cci_sign_of Prename.empty_ren Penv.empty)
+  in
+  Termast.ast_of_constr true env c
 
 let rec coqast_of_program loc = function
   | Var id -> let s = string_of_id id in <:ast< ($VAR $s) >>
@@ -151,7 +155,7 @@ let rec coqast_of_program loc = function
 		   (function Term t -> coqast_of_program t.loc t.desc
 		      | _ -> invalid_arg "coqast_of_program") l
       in
-	<:ast< (APPLIST $f ($LIST $args)) >>
+      <:ast< (APPLIST $f ($LIST $args)) >>
   | Expression c -> bdize c
   | _ -> invalid_arg "coqast_of_program"
 
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 66633277a..6a7a70cf3 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -248,55 +248,29 @@ let register id n =
   let id' = match n with None -> id | Some id' -> id' in
   Penv.register id id'
 
-(*
-let wrap_save_named b =
-  let pf_id = Pfedit.get_current_proof_name () in
-  Command.save_named b;
-  register pf_id None
-
-let wrap_save_anonymous b id =
-  let pf_id = Pfedit.get_current_proof_name () in
-  Command.save_anonymous b (string_of_id id);
-  register pf_id (Some id)
-*)
-
 let _ = 
   let current_save = Vernacinterp.vinterp_map "SaveNamed" in
-    add "SaveNamed"
-      (function [] -> (fun () -> let pf_id =  Pfedit.get_current_proof_name () in
-			 current_save [] ();
-			 register pf_id None)
-	 |   _  -> assert false)
+  add "SaveNamed"
+    (function [] -> (fun () -> let pf_id =  Pfedit.get_current_proof_name () in
+		     current_save [] ();
+		     register pf_id None)
+       |   _  -> assert false)
 
 let _ = 
   let current_defined = Vernacinterp.vinterp_map "DefinedNamed" in
-    add "DefinedNamed"
-      (function [] -> (fun () -> let pf_id = Pfedit.get_current_proof_name () in
-			 current_defined [] ();
-			 register pf_id None)
-	 | _ -> assert false)
+  add "DefinedNamed"
+    (function [] -> (fun () -> let pf_id = Pfedit.get_current_proof_name () in
+		     current_defined [] ();
+		     register pf_id None)
+       | _ -> assert false)
 
 let _ =
   let current_saveanonymous = Vernacinterp.vinterp_map "SaveAnonymous" in
-    add "SaveAnonymous"
-      (function [VARG_IDENTIFIER id] -> 
-	 (fun () -> let pf_id = Pfedit.get_current_proof_name () in
-	    current_saveanonymous [VARG_IDENTIFIER id] ();
-	    register pf_id (Some id))
-    |   _  -> assert false)
-
-(* Old version that does not allow multiple modifications of the "Save" command *)
-(*
-let _ = 
-
-let _ = add "DefinedNamed"
-    (function [] -> (fun () -> if_verbose show_script ();
-		              wrap_save_named false)
-    |   _  -> assert false)
-
-let _ = add "SaveAnonymous"
+  add "SaveAnonymous"
     (function [VARG_IDENTIFIER id] -> 
-       (fun () -> if_verbose show_script ();
-	          wrap_save_anonymous true id)
-    |   _  -> assert false)
-*)
+       (fun () -> 
+	  let pf_id = Pfedit.get_current_proof_name () in
+	  current_saveanonymous [VARG_IDENTIFIER id] ();
+	  register pf_id (Some id))
+       |   _  -> assert false)
+