From b1791fe718eae95897d2dbd160b05285c6df239c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 21 Aug 2016 19:33:03 +0200
Subject: Do not recompute the whole evar naming environment in GProd
 intepretation.

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

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e7f87c5f71..f466740036 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -804,8 +804,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
         let j = pretype_type empty_valcon env evdref lvar c2 in
           { j with utj_val = lift 1 j.utj_val }
       | Name _ ->
-        let var = (name,j.utj_val) in
-        let env' = ExtraEnv.make_env (push_rel_assum var env.ExtraEnv.env) in
+        let var = LocalAssum (name, j.utj_val) in
+        let env' = push_rel var env in
           pretype_type empty_valcon env' evdref lvar c2
     in
     let name = ltac_interp_name lvar name in
-- 
cgit v1.2.3