aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cases.ml')
-rw-r--r--pretyping/cases.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 73be9d6b7..b16f1a9ed 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2581,7 +2581,8 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in
let j =
{ uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
- uj_type = EConstr.of_constr (EConstr.to_constr !evdref tycon); }
+ (* XXX: is this normalization needed? *)
+ uj_type = Evarutil.nf_evar !evdref tycon; }
in j
(**************************************************************************)