From 9228b0b47aa377f05f99b5cc19b8d83af984565f Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 17 Dec 2001 15:17:10 +0000
Subject: le save de Correctness faisant assert false

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2300 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/correctness/ptactic.ml | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index e8f10fc899..097ddd7da2 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -269,10 +269,13 @@ let _ =
 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)
+    (function l -> 
+      (fun () -> 
+        let id = match l with
+            [VARG_IDENTIFIER id] -> id
+          | [_;VARG_IDENTIFIER id] -> id
+          | _ -> assert false in
+	let pf_id = Pfedit.get_current_proof_name () in
+	current_saveanonymous l ();
+	register pf_id (Some id)))
 
-- 
cgit v1.2.3