diff options
Diffstat (limited to 'pretyping/detyping.mli')
| -rw-r--r-- | pretyping/detyping.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 0e9166ac4c..445c2183df 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -40,6 +40,9 @@ val detype_case : val detype_sort : sorts -> rawsort +val detype_rel_context : constr option -> identifier list -> names_context -> + rel_context -> (name * rawconstr option * rawconstr) list + (* 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 val lookup_index_as_renamed : env -> constr -> int -> int option @@ -57,4 +60,3 @@ val simple_cases_matrix_of_branches : inductive -> int list -> rawconstr list -> cases_clauses val return_type_of_predicate : inductive -> int -> int -> rawconstr -> predicate_pattern * rawconstr option - |