From fc2bc9f806ad7627ca2288ae9dfd27512462a5fa Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sat, 22 Dec 2018 00:42:07 +0100
Subject: Make `Add Morphism` not rely on Refine Instance

---
 plugins/ltac/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 4bb52f599a..2055b25ff4 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2014,7 +2014,7 @@ let add_morphism atts binders m s n =
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
   ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance
-           (Some (true, CAst.make @@ CRecord []))
+     None
     ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
 
 (** Bind to "rewrite" too *)
-- 
cgit v1.2.3