aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.mli
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-11 20:01:04 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-11 20:01:04 +0000
commit0601db38b579513e4ab39a161591cd359260490e (patch)
tree2741c3b805ec8b890c5b9f58aeb1445ec10590fc /pretyping/cases.mli
parent8556f4e4b5e21535013e6962feabfede6313462b (diff)
Promote evar_defs to evar_map (in Evd)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7
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