From 1ed0836a7e0c8e05b0288f85e344ef5249d5d228 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 10 Nov 2017 13:23:32 +0100
Subject: Inference of inductive subtyping does not need an evar map.

---
 interp/declare.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index 55f825c251..0bfc9060b8 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -364,13 +364,8 @@ let infer_inductive_subtyping (pth, mind_ent) =
   | Cumulative_ind_entry cumi ->
     begin
       let env = Global.env () in
-      let env' =
-        Environ.push_context
-          (Univ.CumulativityInfo.univ_context cumi) env
-      in
       (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
-      let evd = Evd.from_env env' in
-        (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent)
+        (pth, Inductiveops.infer_inductive_subtyping env mind_ent)
     end
 
 type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
-- 
cgit v1.2.3