rewrite/Univs: Fix bug # 4498.

2 files changed, 36 insertions, 11 deletions

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 9d70c177b4..c7cfc4dc72 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1799,10 +1799,10 @@ let declare_projection n instance_id r =
   let poly = Global.is_polymorphic r in
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let evd,c = Evd.fresh_global env sigma r in
+  let sigma,c = Evd.fresh_global env sigma r in
   let ty = Retyping.get_type_of env sigma c in
   let term = proper_projection c ty in
-  let typ = Typing.unsafe_type_of env sigma term in
+  let sigma, typ = Typing.type_of env sigma term in
   let ctx, typ = decompose_prod_assum typ in
   let typ =
     let n =
@@ -1831,9 +1831,7 @@ let declare_projection n instance_id r =
     ignore(Declare.declare_constant n 
 	   (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
 
-let build_morphism_signature m =
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
+let build_morphism_signature env sigma m =
   let m,ctx = Constrintern.interp_constr env sigma m in
   let sigma = Evd.from_ctx ctx in
   let t = Typing.unsafe_type_of env sigma m in
@@ -1858,8 +1856,10 @@ let build_morphism_signature m =
   in
   let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in
   let evd = solve_constraints env !evd in
-  let m = Evarutil.nf_evar evd morph in
-    Evarutil.check_evars env Evd.empty evd m; m
+  let evd = Evd.nf_constraints evd in
+  let m = Evarutil.nf_evars_universes evd morph in
+  Evarutil.check_evars env Evd.empty evd m;
+  Evd.evar_universe_context evd, m
 
 let default_morphism sign m =
   let env = Global.env () in
@@ -1896,12 +1896,13 @@ let add_morphism_infer glob m n =
   init_setoid ();
   let poly = Flags.is_universe_polymorphism () in
   let instance_id = add_suffix n "_Proper" in
-  let instance = build_morphism_signature m in
-  let evd = Evd.from_env (Global.env ()) in
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let uctx, instance = build_morphism_signature env evd m in
     if Lib.is_modtype () then
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
 				(Entries.ParameterEntry 
-				 (None,poly,(instance,Univ.UContext.empty),None), 
+				 (None,poly,(instance,Evd.evar_context_universe_context uctx),None), 
 				 Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
 	add_instance (Typeclasses.new_instance 
@@ -1924,7 +1925,7 @@ let add_morphism_infer glob m n =
       let hook = Lemmas.mk_hook hook in
 	Flags.silently
 	  (fun () ->
-	    Lemmas.start_proof instance_id kind evd instance hook;
+	    Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) instance hook;
 	    ignore (Pfedit.by (Tacinterp.interp tac))) ()
 
 let add_morphism glob binders m s n =
diff --git a/test-suite/bugs/closed/4498.v b/test-suite/bugs/closed/4498.v
new file mode 100644
index 0000000000..ccdb2dddda
--- /dev/null
+++ b/test-suite/bugs/closed/4498.v
@@ -0,0 +1,24 @@
+Require Export Coq.Unicode.Utf8.
+Require Export Coq.Classes.Morphisms.
+Require Export Coq.Relations.Relation_Definitions.
+
+Set Universe Polymorphism.
+
+Reserved Notation "a ~> b" (at level 90, right associativity).
+
+Class Category := {
+  ob            : Type;
+  uhom          := Type : Type;
+  hom           : ob → ob → uhom where "a ~> b" := (hom a b);
+  compose       : ∀ {A B C}, (B ~> C) → (A ~> B) → (A ~> C);
+  equiv         : ∀ {A B}, relation (A ~> B);
+  is_equiv      : ∀ {A B}, @Equivalence (A ~> B) equiv;
+  comp_respects : ∀ {A B C},
+      Proper (@equiv B C ==> @equiv A B ==> @equiv A C) (@compose A B C);
+}.
+
+Require Export Coq.Setoids.Setoid.
+
+Add Parametric Morphism `{C : Category} {A B C} : (@compose _ A B C) with
+  signature equiv ==> equiv ==> equiv as compose_mor.
+Proof. apply comp_respects. Qed.
\ No newline at end of file