From bb78a36d77ff37ba9fc11d6db914ee4bc71e3e2e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 13 Apr 2018 18:01:02 +0200
Subject: Relying on the precomputation of the renaming also for new_evar_type.

---
 pretyping/cases.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'pretyping/cases.ml')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 668c2770d2..7baa755ab5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -406,9 +406,14 @@ let coerce_to_indtype typing_fun evdref env matx tomatchl =
 (* Utils *)
 
 let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref =
-  let (e, u) = evd_comb1 (new_type_evar env  ~src:src) evdref univ_flexible_alg in
+  let (e, u) = evd_comb1 (new_type_evar env ~src:src) evdref univ_flexible_alg in
   e
 
+let evd_comb2 f evdref x y =
+  let (evd',y) = f !evdref x y in
+  evdref := evd';
+  y
+
 let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
   (* Ideally, we could find a common inductive type to which both the
      term to match and the patterns coerce *)
-- 
cgit v1.2.3