Relying on the precomputation of the renaming also for new_evar_type.

1 files changed, 6 insertions, 1 deletions

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 *)