diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index d80bacbfbe..0084fce652 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -142,6 +142,7 @@ type ml_case_error = exception NotInferable of ml_case_error + let pred_case_ml env sigma isrec (IndType (indf,realargs)) (i,ft) = let pred = let (ind,params) = dest_ind_family indf in |