From 7f207c26b603a40ecbb58377f6669935d0419366 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 8 Dec 2014 13:52:23 +0100
Subject: Fixing wrong evar_map in return clause inference, revealed by
 48509b611.

---
 pretyping/cases.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0005f83919..eeb367a43d 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1587,8 +1587,7 @@ let rec list_assoc_in_triple x = function
 *)
 
 let abstract_tycon loc env evdref subst _tycon extenv t =
-  let sigma = !evdref in
-  let t = nf_betaiota sigma t in (* it helps in some cases to remove K-redex *)
+  let t = nf_betaiota !evdref t in (* it helps in some cases to remove K-redex *)
   let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv subst t in
   (* We traverse the type T of the original problem Xi looking for subterms
      that match the non-constructor part of the constraints (this part
@@ -1600,7 +1599,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
     | Rel n when pi2 (lookup_rel n env) != None ->
         map_constr_with_full_binders push_binder aux x t
     | Evar ev ->
-        let ty = get_type_of env sigma t in
+        let ty = get_type_of env !evdref t in
 	let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in
         let inst =
 	  List.map_i
@@ -1614,7 +1613,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
         end;
         ev'
     | _ ->
-    let good = List.filter (fun (_,u,_) -> is_conv_leq env sigma t u) subst in
+    let good = List.filter (fun (_,u,_) -> is_conv_leq env !evdref t u) subst in
     match good with
     | [] ->
       map_constr_with_full_binders push_binder aux x t
-- 
cgit v1.2.3