diff options
-rw-r--r-- | tactics/tactics.ml | 52 |
1 files changed, 25 insertions, 27 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 282e417c3..9e25055e9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2464,36 +2464,34 @@ let abstract_subproof name tac gls = let sign,secsign = List.fold_right (fun (id,_,_ as d) (s1,s2) -> - if mem_named_context id current_sign & - interpretable_as_section_decl (Sign.lookup_named id current_sign) d - then (s1,push_named_context_val d s2) - else (add_named_decl d s1,s2)) + if mem_named_context id current_sign & + interpretable_as_section_decl (Sign.lookup_named id current_sign) d + then (s1,push_named_context_val d s2) + else (add_named_decl d s1,s2)) global_sign (empty_named_context,empty_named_context_val) in let na = next_global_ident_away false name (pf_ids_of_hyps gls) in let concl = it_mkNamedProd_or_LetIn (pf_concl gls) sign in - if occur_existential concl then - error "\"abstract\" cannot handle existentials"; - let lemme = - start_proof na (Global, Proof Lemma) secsign concl (fun _ _ -> ()); - let _,(const,kind,_) = - try - by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); - let r = cook_proof () in - delete_current_proof (); r - with - e when catchable_exception e -> - (delete_current_proof(); raise e) - | FailError (0,_) as e -> - (delete_current_proof(); raise e) - in (* Faudrait un peu fonctionnaliser cela *) - let cd = Entries.DefinitionEntry const in - let con = Declare.declare_internal_constant na (cd,IsProof Lemma) in - constr_of_global (ConstRef con) - in - exact_no_check - (applist (lemme, - List.rev (Array.to_list (instance_from_named_context sign)))) - gls + if occur_existential concl then + error "\"abstract\" cannot handle existentials"; + let lemme = + start_proof na (Global, Proof Lemma) secsign concl (fun _ _ -> ()); + let _,(const,kind,_) = + try + by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); + let r = cook_proof () in + delete_current_proof (); r + with + e -> + (delete_current_proof(); raise e) + in (* Faudrait un peu fonctionnaliser cela *) + let cd = Entries.DefinitionEntry const in + let con = Declare.declare_internal_constant na (cd,IsProof Lemma) in + constr_of_global (ConstRef con) + in + exact_no_check + (applist (lemme, + List.rev (Array.to_list (instance_from_named_context sign)))) + gls let tclABSTRACT name_op tac gls = let s = match name_op with |