diff options
Diffstat (limited to 'pretyping/detyping.mli')
| -rw-r--r-- | pretyping/detyping.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 13d37c8436..5cf174875a 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -29,7 +29,7 @@ val detype_case : 'a -> Rawterm.loc * Names.identifier list * Rawterm.cases_pattern list * Rawterm.rawconstr) -> env -> identifier list -> names_context -> inductive -> case_style -> - 'a option -> 'a -> 'a array -> rawconstr + 'a option -> int -> 'a -> 'a array -> rawconstr (* look for the index of a named var or a nondep var as it is renamed *) val lookup_name_as_renamed : env -> constr -> identifier -> int option |