diff options
| -rw-r--r-- | interp/topconstr.ml | 5 | ||||
| -rw-r--r-- | interp/topconstr.mli | 2 |
2 files changed, 7 insertions, 0 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index ad21e5b371..61e03fb3f7 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -99,6 +99,11 @@ let rawconstr_of_aconstr_with_binders loc g f e = function | APatVar n -> RPatVar (loc,(false,n)) | ARef x -> RRef (loc,x) +let rec rawconstr_of_aconstr loc x = + let rec aux () x = + rawconstr_of_aconstr_with_binders loc (fun id () -> (id,())) aux () x + in aux () x + let rec subst_pat subst pat = match pat with | PatVar _ -> pat diff --git a/interp/topconstr.mli b/interp/topconstr.mli index c7cc74b0f8..84342b2209 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -47,6 +47,8 @@ val rawconstr_of_aconstr_with_binders : loc -> (identifier -> 'a -> identifier * 'a) -> ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr +val rawconstr_of_aconstr : loc -> aconstr -> rawconstr + val subst_aconstr : substitution -> Names.identifier list -> aconstr -> aconstr val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr |