From 85aca1dda24c5933d803b195570514df219e51d8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Oct 2019 15:24:32 +0100
Subject: Return of Refine Instance as an attribute.

We can now do `#[refine] Instance : Bla := bli.` to enter proof mode
with `bli` as a starting refinement.

If `bli` is enough to define the instance we still enter proof mode,
keeping things nicely predictable for the stm.
---
 plugins/ltac/rewrite.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 1493092f2f..6be358be21 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2023,7 +2023,8 @@ let add_morphism atts binders m s n =
   let _id, lemma = Classes.new_instance_interactive
       ~global:atts.global ~poly:atts.polymorphic
       instance_name binders instance_t
-      ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
+      ~generalize:false ~tac ~hook:(declare_projection n instance_id)
+      Hints.empty_hint_info None
   in
   lemma (* no instance body -> always open proof *)
 
-- 
cgit v1.2.3