diff options
Diffstat (limited to 'contrib/funind/rawtermops.mli')
| -rw-r--r-- | contrib/funind/rawtermops.mli | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli index 9647640c..358c6ba6 100644 --- a/contrib/funind/rawtermops.mli +++ b/contrib/funind/rawtermops.mli @@ -22,7 +22,7 @@ val mkRApp : rawconstr*(rawconstr list) -> rawconstr val mkRLambda : Names.name*rawconstr*rawconstr -> rawconstr val mkRProd : Names.name*rawconstr*rawconstr -> rawconstr val mkRLetIn : Names.name*rawconstr*rawconstr -> rawconstr -val mkRCases : rawconstr option * tomatch_tuple * cases_clauses -> rawconstr +val mkRCases : rawconstr option * tomatch_tuples * cases_clauses -> rawconstr val mkRSort : rawsort -> rawconstr val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *) val mkRCast : rawconstr* rawconstr -> rawconstr @@ -31,8 +31,14 @@ val mkRCast : rawconstr* rawconstr -> rawconstr These are analogous to the ones constrs *) val raw_decompose_prod : rawconstr -> (Names.name*rawconstr) list * rawconstr +val raw_decompose_prod_or_letin : + rawconstr -> (Names.name*rawconstr option*rawconstr option) list * rawconstr val raw_decompose_prod_n : int -> rawconstr -> (Names.name*rawconstr) list * rawconstr +val raw_decompose_prod_or_letin_n : int -> rawconstr -> + (Names.name*rawconstr option*rawconstr option) list * rawconstr val raw_compose_prod : rawconstr -> (Names.name*rawconstr) list -> rawconstr +val raw_compose_prod_or_letin: rawconstr -> + (Names.name*rawconstr option*rawconstr option) list -> rawconstr val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list) |