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.
---
 stm/vernac_classifier.ml | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

(limited to 'stm')

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 24976d8c1f..ff0bf0ac2a 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -183,12 +183,16 @@ let classify_vernac e =
     | VernacDeclareMLModule _
     | VernacContext _ (* TASSI: unsure *) -> VtSideff ([], VtNow)
     | VernacProofMode pm -> VtProofMode pm
-    | VernacInstance ((name,_),_,_,None,_) when not (Attributes.parse_drop_extra Attributes.program atts) ->
-      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
-      let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-      VtStartProof (guarantee, idents_of_name name.CAst.v)
-    | VernacInstance ((name,_),_,_,_,_) ->
-      VtSideff (idents_of_name name.CAst.v, VtLater)
+    | VernacInstance ((name,_),_,_,props,_) ->
+      let program, refine =
+        Attributes.(parse_drop_extra Notations.(program ++ Classes.refine_att) atts)
+      in
+      if program || (props <> None && not refine) then
+        VtSideff (idents_of_name name.CAst.v, VtLater)
+      else
+        let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+        let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+        VtStartProof (guarantee, idents_of_name name.CAst.v)
     (* Stm will install a new classifier to handle these *)
     | VernacBack _ | VernacAbortAll
     | VernacUndoTo _ | VernacUndo _
-- 
cgit v1.2.3