diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cd618ed988..4e6a293c98 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3391,7 +3391,7 @@ let abstract_subproof id tac gl = try flush_and_check_evars (project gl) concl with Uninstantiated_evar _ -> error "\"abstract\" cannot handle existentials." in - let const = Pfedit.build_constant_by_tactic secsign concl + let const = Pfedit.build_constant_by_tactic id secsign concl (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)) in let cd = Entries.DefinitionEntry const in let lem = mkConst (Declare.declare_constant ~internal:Declare.KernelSilent id (cd,IsProof Lemma)) in |