diff options
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 8f9360e578..4ce07815e1 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 53182e34b8..a3224128a8 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 |