[declare] [rewrite] Use high-level declare API, part II.

1 files changed, 14 insertions, 15 deletions

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 68cac786e4..d72dcf8120 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1924,10 +1924,7 @@ let build_morphism_signature env sigma m =
   in
   let morph = e_app_poly env evd (PropGlobal.proper_type env) [| t; sig_; m |] in
   let evd = solve_constraints env !evd in
-  let evd = Evd.minimize_universes evd in
-  let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in
-  Pretyping.check_evars env evd (EConstr.of_constr m);
-  Evd.evar_universe_context evd, m
+  evd, morph
 
 let default_morphism sign m =
   let env = Global.env () in
@@ -1962,22 +1959,24 @@ let add_morphism_as_parameter atts m n : unit =
   let instance_id = add_suffix n "_Proper" in
   let env = Global.env () in
   let evd = Evd.from_env env in
-  let uctx, instance = build_morphism_signature env evd m in
-  let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
-  let cst = Declare.declare_constant ~name:instance_id
-      ~kind:Decls.(IsAssumption Logical)
-      (Declare.ParameterEntry (None,(instance,uctx),None))
-  in
-  Classes.add_instance (Classes.mk_instance
-                  (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (GlobRef.ConstRef cst));
-  declare_projection n instance_id (GlobRef.ConstRef cst)
+  let poly = atts.polymorphic in
+  let kind, opaque, scope = Decls.(IsAssumption Logical), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+  let impargs, udecl = [], UState.default_univ_decl in
+  let evd, types = build_morphism_signature env evd m in
+  let evd, pe = DeclareDef.prepare_parameter ~poly ~udecl ~types evd in
+  let cst = Declare.declare_constant ~name:instance_id ~kind (Declare.ParameterEntry pe) in
+  let cst = GlobRef.ConstRef cst in
+  Classes.add_instance
+    (Classes.mk_instance
+       (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global cst);
+  declare_projection n instance_id cst
 
 let add_morphism_interactive atts m n : Lemmas.t =
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
   let env = Global.env () in
   let evd = Evd.from_env env in
-  let uctx, instance = build_morphism_signature env evd m in
+  let evd, morph = build_morphism_signature env evd m in
   let poly = atts.polymorphic in
   let kind = Decls.(IsDefinition Instance) in
   let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
@@ -1993,7 +1992,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
   let info = Lemmas.Info.make ~hook ~kind () in
   Flags.silently
     (fun () ->
-       let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+       let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info evd morph in
        fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =