diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
3 files changed, 4 insertions, 4 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 00dc193325..d447a97e85 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1860,7 +1860,7 @@ let subst_induction_arg subst = function let subst_evaluable_reference subst = function | EvalVarRef id -> EvalVarRef id - | EvalConstRef kn -> EvalConstRef (subst_kn subst kn) + | EvalConstRef kn -> EvalConstRef (subst_con subst kn) let subst_and_short_name f (c,n) = assert (n=None); (* since tacdef are strictly globalized *) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 0a0589e967..e30bb7e63b 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -339,7 +339,7 @@ let general_elim_then_using | _ -> let name_elim = match kind_of_term elim with - | Const kn -> string_of_kn kn + | Const kn -> string_of_con kn | Var id -> string_of_id id | _ -> "\b" in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index dc2865be49..314bcd55f8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1880,9 +1880,9 @@ let abstract_subproof name tac gls = (delete_current_proof(); raise e) in (* Faudrait un peu fonctionnaliser cela *) let cd = Entries.DefinitionEntry const in - let sp = Declare.declare_internal_constant na (cd,IsProof Lemma) in + let con = Declare.declare_internal_constant na (cd,IsProof Lemma) in let newenv = Global.env() in - constr_of_reference (ConstRef (snd sp)) + constr_of_reference (ConstRef con) in exact_no_check (applist (lemme, |