aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cases.mli')
-rw-r--r--pretyping/cases.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index e6d42e10d..669240312 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -64,7 +64,7 @@ type tomatch_status =
module type S = sig
val compile_cases :
loc -> case_style ->
- (type_constraint -> env -> evar_defs ref -> rawconstr -> unsafe_judgment) * evar_defs ref ->
+ (type_constraint -> env -> evar_map ref -> rawconstr -> unsafe_judgment) * evar_map ref ->
type_constraint ->
env -> rawconstr option * tomatch_tuples * cases_clauses ->
unsafe_judgment