Univs: fix bug #5188

Parameter was implemented the wrong way trying to separate the universes
of the telescope.

2 files changed, 12 insertions, 8 deletions

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