diff options
| author | herbelin | 2006-01-08 17:13:38 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-08 17:13:38 +0000 |
| commit | a4f64ba3e82546d2cc57b6c2be4bad0d52364863 (patch) | |
| tree | 1585a4e23f92637e03db9ca08528e62768fcce5a | |
| parent | 17b904b53e9cdd09c03d59ff94205d84a44c81b8 (diff) | |
Ajout rawconstr_of_aconstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7817 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |