diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/indrec.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/library/indrec.mli b/library/indrec.mli index 1722bef12a..da2ae3102c 100644 --- a/library/indrec.mli +++ b/library/indrec.mli @@ -52,3 +52,8 @@ val pred_case_ml_onebranch : unsafe_env ->'c evar_map -> bool -> val make_case_ml : bool -> constr -> constr -> case_info -> constr array -> constr + + +(*s Auxiliary functions. TODO: les déplacer ailleurs. *) + +val prod_create : unsafe_env -> constr * constr -> constr |