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/declare.ml')

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


From 6c2d10b93b819f0735a43453c78566795de8ba5a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 10 Nov 2017 15:05:21 +0100
Subject: Use specialized function for inductive subtyping inference.

This ensures by construction that we never infer constraints outside
the variance model.
---
 interp/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/declare.ml')

diff --git a/interp/declare.ml b/interp/declare.ml
index 0bfc9060b8..72cdabfd20 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -365,7 +365,7 @@ let infer_inductive_subtyping (pth, mind_ent) =
     begin
       let env = Global.env () in
       (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
-        (pth, Inductiveops.infer_inductive_subtyping env mind_ent)
+        (pth, InferCumulativity.infer_inductive env mind_ent)
     end
 
 type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
-- 
cgit v1.2.3