diff options
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index cea769955..a9a51d9ac 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -110,7 +110,7 @@ val type_case_branches_with_names : types array * types val make_case_info : env -> inductive -> case_style -> case_info -(*i Compatibility +(*i Compatibility val make_default_case_info : env -> case_style -> inductive -> case_info i*) |