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/globEnv.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'pretyping/globEnv.ml')

diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 57bedf1ee9..12788e5ec5 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -107,6 +107,11 @@ let e_new_evar env evdref ?src ?naming typ =
   evdref := sigma;
   e
 
+let e_new_type_evar env evdref ~src =
+  let (evd', s) = Evd.new_sort_variable Evd.univ_flexible_alg !evdref in
+  evdref := evd';
+  e_new_evar env evdref ~src (EConstr.mkSort s)
+
 let hide_variable env expansion id =
   let lvar = env.lvar in
   if Id.Map.mem id lvar.ltac_genargs then
-- 
cgit v1.2.3