diff options
Diffstat (limited to 'pretyping/cases.mli')
| -rw-r--r-- | pretyping/cases.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index a7dddb5cb..7e5fda903 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -35,7 +35,7 @@ val branch_scheme : env -> 'a evar_defs -> bool -> inductive_family -> constr array val pred_case_ml_onebranch : loc -> env -> 'c evar_map -> bool -> - inductive_type -> int * constr * constr -> constr + inductive_type -> int * unsafe_judgment -> constr (* Compilation of pattern-matching. *) |