diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-17 15:17:10 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-17 15:17:10 +0000 |
| commit | 9228b0b47aa377f05f99b5cc19b8d83af984565f (patch) | |
| tree | cab33494e1e483d3ee4d2933b399ec7233a17fac /contrib | |
| parent | e6d2309432e62b38d689777c28ef84ce495c8b27 (diff) | |
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
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/correctness/ptactic.ml | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index e8f10fc89..097ddd7da 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))) |