diff options
Diffstat (limited to 'pretyping/detyping.mli')
| -rw-r--r-- | pretyping/detyping.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 445c2183d..588bc8c84 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -50,8 +50,6 @@ val lookup_index_as_renamed : env -> constr -> int -> int option val set_detype_anonymous : (loc -> int -> rawconstr) -> unit val force_wildcard : unit -> bool val synthetize_type : unit -> bool -val force_if : case_info -> bool -val force_let : case_info -> bool (* Utilities to transform kernel cases to simple pattern-matching problem *) |