diff options
Diffstat (limited to 'contrib/correctness/ptactic.ml')
| -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))) |