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 /interp | |
| 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 'interp')
| -rw-r--r-- | interp/topconstr.ml | 1 | ||||
| -rw-r--r-- | interp/topconstr.mli | 3 |
2 files changed, 3 insertions, 1 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 8f9360e57..4ce07815e 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -16,6 +16,7 @@ open Nameops open Libnames open Rawterm open Term +open Mod_subst (*i*) (**********************************************************************) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 53182e34b..a3224128a 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -15,6 +15,7 @@ open Names open Libnames open Rawterm open Term +open Mod_subst (*i*) (*s This is the subtype of rawconstr allowed in syntactic extensions *) @@ -47,7 +48,7 @@ val rawconstr_of_aconstr_with_binders : loc -> (identifier -> 'a -> identifier * 'a) -> ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr -val subst_aconstr : Names.substitution -> aconstr -> aconstr +val subst_aconstr : substitution -> aconstr -> aconstr val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr |