nettoyage

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

1 files changed, 17 insertions, 43 deletions

diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 66633277a9..6a7a70cf3e 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)
+