diff options
| author | sacerdot | 2004-11-16 12:37:40 +0000 |
|---|---|---|
| committer | sacerdot | 2004-11-16 12:37:40 +0000 |
| commit | d6c204c70c3b89b5bda4e7779cc4a20b5fa3f63f (patch) | |
| tree | ed4d954a685588ee55f4d8902eba8a1afc864472 /tactics | |
| parent | 08cb37edb71af0301a72acc834d50f24b0733db5 (diff) | |
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
MOVITATION: in a forthcoming commit the application of a substitution to a
constant will return a constr and not a constant. The application of a
substitution to a kernel_name will return a kernel_name. Thus "constant"
should be use as a kernel name for references that can be delta-expanded.
KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code
that implements "Canonical Structure"s). The ADT is violated once in this
ocaml module. My feeling is that the implementation of "Canonical Structure"s
should be rewritten to avoid this situation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
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, |