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.

1 files changed, 10 insertions, 6 deletions

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 _