From af58f731322527af1d81233beade4c98fbb2d7bd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 28 Nov 2016 19:05:23 +0100
Subject: Univs: fix bug #5188

Parameter was implemented the wrong way trying to separate the universes
of the telescope.
---
 test-suite/bugs/closed/5188.v |  5 +++++
 toplevel/command.ml           | 15 +++++++--------
 2 files changed, 12 insertions(+), 8 deletions(-)
 create mode 100644 test-suite/bugs/closed/5188.v

diff --git a/test-suite/bugs/closed/5188.v b/test-suite/bugs/closed/5188.v
new file mode 100644
index 0000000000..e29ebfb4ec
--- /dev/null
+++ b/test-suite/bugs/closed/5188.v
@@ -0,0 +1,5 @@
+Set Printing All.
+Axiom relation : forall (T : Type), Set.
+Axiom T : forall A (R : relation A), Set.
+Set Printing Universes.
+Parameter (A:_) (R:_) (e:@T A R).
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7ffe680e5e..f6172a4b85 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -261,10 +261,7 @@ match local with
 
 let interp_assumption evdref env impls bl c =
   let c = prod_constr_expr c bl in
-  let ty, impls = interp_type_evars_impls env evdref ~impls c in
-  let evd, nf = nf_evars_and_universes !evdref in
-  let ctx = Evd.universe_context_set evd in
-    ((nf ty, ctx), impls)
+  interp_type_evars_impls env evdref ~impls c
 
 let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl =
   let refs, status, _ =
@@ -290,25 +287,27 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
     else l
   in
   let _,l = List.fold_map (fun (env,ienv) (is_coe,(idl,c)) ->
-    let (t,ctx),imps = interp_assumption evdref env ienv [] c in
+    let t,imps = interp_assumption evdref env ienv [] c in
     let env =
       push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in
     let ienv = List.fold_right (fun (_,id) ienv ->
       let impls = compute_internalization_data env Variable t imps in
       Id.Map.add id impls ienv) idl ienv in
-      ((env,ienv),((is_coe,idl),t,(ctx,imps)))) 
+      ((env,ienv),((is_coe,idl),t,imps))) 
     (env,empty_internalization_env) l
   in
   let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in
+  let evd = Evd.nf_constraints evd in
+  let ctx = Evd.universe_context_set evd in
   let l = List.map (on_pi2 (nf_evar evd)) l in
-  snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) ->
+  pi2 (List.fold_left (fun (subst,status,ctx) ((is_coe,idl),t,imps) ->
     let t = replace_vars subst t in
     let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in
     let subst' = List.map2 
       (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u)))
       idl refs 
     in
-      (subst'@subst, status' && status)) ([],true) l)
+      (subst'@subst, status' && status, Univ.ContextSet.empty)) ([],true,ctx) l)
 
 let do_assumptions_bound_univs coe kind nl id pl c =
   let env = Global.env () in
-- 
cgit v1.2.3


From f492ddb3f9949993ad9072688e9e2cac7cfcbce0 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 2 Dec 2016 16:46:05 +0100
Subject: Comment on universe handling in Parameters

---
 toplevel/command.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/toplevel/command.ml b/toplevel/command.ml
index f6172a4b85..8b527ebd6f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -286,6 +286,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
         l []
     else l
   in
+  (* We intepret all declarations in the same evar_map, i.e. as a telescope. *)
   let _,l = List.fold_map (fun (env,ienv) (is_coe,(idl,c)) ->
     let t,imps = interp_assumption evdref env ienv [] c in
     let env =
@@ -297,6 +298,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
     (env,empty_internalization_env) l
   in
   let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in
+  (* The universe constraints come from the whole telescope. *)
   let evd = Evd.nf_constraints evd in
   let ctx = Evd.universe_context_set evd in
   let l = List.map (on_pi2 (nf_evar evd)) l in
@@ -307,7 +309,9 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
       (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u)))
       idl refs 
     in
-      (subst'@subst, status' && status, Univ.ContextSet.empty)) ([],true,ctx) l)
+    (subst'@subst, status' && status,
+     (* The universe constraints are declared with the first declaration only. *)
+     Univ.ContextSet.empty)) ([],true,ctx) l)
 
 let do_assumptions_bound_univs coe kind nl id pl c =
   let env = Global.env () in
-- 
cgit v1.2.3