diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-16 15:49:08 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-16 15:49:08 +0000 |
| commit | b01b06d3a843c97adc6c0a0621b8d681c10fa6fe (patch) | |
| tree | d3f90b1dc590ffd917090290d9fd03e63c094a49 /kernel/declarations.ml | |
| parent | d6c204c70c3b89b5bda4e7779cc4a20b5fa3f63f (diff) | |
Names.substitution (and related functions) and Term.subst_mps moved to
the new module kernel/mod_subst.ml.
MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now
possible to define substitutions that also delta-expand constants
(by associating the delta-expanded form to the constant name).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index b5505bce3..72f37e226 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -14,6 +14,7 @@ open Names open Univ open Term open Sign +open Mod_subst (*i*) (* This module defines the types of global declarations. This includes @@ -109,7 +110,7 @@ type mutual_inductive_body = { let subst_const_body sub cb = { const_hyps = (assert (cb.const_hyps=[]); []); const_body = option_app (subst_constr_subst sub) cb.const_body; - const_type = type_app (Term.subst_mps sub) cb.const_type; + const_type = type_app (subst_mps sub) cb.const_type; const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*) const_constraints = cb.const_constraints; @@ -119,17 +120,17 @@ let subst_mind_packet sub mbp = { mind_consnames = mbp.mind_consnames; mind_typename = mbp.mind_typename; mind_nf_lc = - array_smartmap (type_app (Term.subst_mps sub)) mbp.mind_nf_lc; - mind_nf_arity = type_app (Term.subst_mps sub) mbp.mind_nf_arity; + array_smartmap (type_app (subst_mps sub)) mbp.mind_nf_lc; + mind_nf_arity = type_app (subst_mps sub) mbp.mind_nf_arity; mind_user_lc = - array_smartmap (type_app (Term.subst_mps sub)) mbp.mind_user_lc; - mind_user_arity = type_app (Term.subst_mps sub) mbp.mind_user_arity; + array_smartmap (type_app (subst_mps sub)) mbp.mind_user_lc; + mind_user_arity = type_app (subst_mps sub) mbp.mind_user_arity; mind_sort = mbp.mind_sort; mind_nrealargs = mbp.mind_nrealargs; mind_kelim = mbp.mind_kelim; mind_nparams = mbp.mind_nparams; mind_params_ctxt = - map_rel_context (Term.subst_mps sub) mbp.mind_params_ctxt; + map_rel_context (subst_mps sub) mbp.mind_params_ctxt; mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); mind_nb_constant = mbp.mind_nb_constant; mind_nb_args = mbp.mind_nb_args; |