[rewrite] Add Morphism syntax made different for module type parameters

3 files changed, 43 insertions, 34 deletions

diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index bb29323858..1a84158df7 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -276,10 +276,14 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
      {
          add_setoid atts binders a aeq t n
      }
-  | #[ atts = rewrite_attributes; ] ![ maybe_open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
-    (* This command may or may not open a goal *)
-    => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater }
-    -> { add_morphism_infer atts m n }
+  | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
+    => { VtStartProof(GuaranteesOpacity, [n]), VtLater }
+    -> { if Lib.is_modtype () then
+           CErrors.user_err Pp.(str "Add Morphism cannot be used in a module type. Use Parameter Morphism instead.");
+         add_morphism_interactive atts m n }
+  | #[ atts = rewrite_attributes; ] [ "Declare" "Morphism" constr(m) ":" ident(n) ]
+    => { VtSideff([n]), VtLater }
+    -> { add_morphism_as_parameter atts m n }
   | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
     => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
     -> { add_morphism atts [] m s n }
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 26d477fee0..c568f63903 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1973,42 +1973,46 @@ let warn_add_morphism_deprecated =
   CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
       Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id"))
 
-let add_morphism_infer atts m n : Proof_global.t option =
+let add_morphism_as_parameter atts m n : unit =
+  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 uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
+  let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
+      (Entries.ParameterEntry
+         (None,(instance,uctx),None),
+       Decl_kinds.IsAssumption Decl_kinds.Logical)
+  in
+  Classes.add_instance (Classes.mk_instance
+                  (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
+  declare_projection n instance_id (ConstRef cst)
+
+let add_morphism_interactive atts m n : Proof_global.t =
   warn_add_morphism_deprecated ?loc:m.CAst.loc ();
   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
-    if Lib.is_modtype () then
-      let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
-      let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
-          (Entries.ParameterEntry
-             (None,(instance,uctx),None),
-           Decl_kinds.IsAssumption Decl_kinds.Logical)
-      in
+  let kind = Decl_kinds.Global, atts.polymorphic,
+             Decl_kinds.DefinitionBody Decl_kinds.Instance
+  in
+  let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
+  let hook _ _ _ = function
+    | Globnames.ConstRef cst ->
       Classes.add_instance (Classes.mk_instance
-                      (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
-      declare_projection n instance_id (ConstRef cst);
-      None
-    else
-      let kind = Decl_kinds.Global, atts.polymorphic,
-                 Decl_kinds.DefinitionBody Decl_kinds.Instance
-      in
-      let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
-      let hook _ _ _ = function
-        | Globnames.ConstRef cst ->
-          Classes.add_instance (Classes.mk_instance
-                          (PropGlobal.proper_class env evd) Hints.empty_hint_info
-                          atts.global (ConstRef cst));
-          declare_projection n instance_id (ConstRef cst)
-        | _ -> assert false
-      in
-      let hook = Lemmas.mk_hook hook in
-      Flags.silently
-        (fun () ->
-           let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
-           Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) ()
+                      (PropGlobal.proper_class env evd) Hints.empty_hint_info
+                      atts.global (ConstRef cst));
+      declare_projection n instance_id (ConstRef cst)
+    | _ -> assert false
+  in
+  let hook = Lemmas.mk_hook hook in
+  Flags.silently
+    (fun () ->
+       let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+       fst Pfedit.(by (Tacinterp.interp tac) pstate)) ()
 
 let add_morphism atts binders m s n =
   init_setoid ();
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 5aabb946d5..3ef33c6dc9 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -101,7 +101,8 @@ val add_setoid
   -> Id.t
   -> unit
 
-val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option
+val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t
+val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit
 
 val add_morphism
   : rewrite_attributes