diff options
Diffstat (limited to 'contrib/funind/rawtermops.mli')
| -rw-r--r-- | contrib/funind/rawtermops.mli | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli index 5dcdb15c..aa355485 100644 --- a/contrib/funind/rawtermops.mli +++ b/contrib/funind/rawtermops.mli @@ -25,7 +25,7 @@ val mkRLetIn : Names.name*rawconstr*rawconstr -> rawconstr val mkRCases : rawconstr option * tomatch_tuple * cases_clauses -> rawconstr val mkRSort : rawsort -> rawconstr val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *) - +val mkRCast : rawconstr* rawconstr -> rawconstr (* Some basic functions to decompose rawconstrs These are analogous to the ones constrs @@ -36,7 +36,7 @@ val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list) (* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *) -val raw_make_eq : rawconstr -> rawconstr -> rawconstr +val raw_make_eq : ?typ:rawconstr -> rawconstr -> rawconstr -> rawconstr (* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *) val raw_make_neq : rawconstr -> rawconstr -> rawconstr (* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *) @@ -106,3 +106,9 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool returns the set of variables appearing in a pattern *) val ids_of_pat : cases_pattern -> Names.Idset.t + + +(* + removing let_in construction in a rawterm +*) +val zeta_normalize : Rawterm.rawconstr -> Rawterm.rawconstr |