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, 23 insertions, 0 deletions

diff --git a/test-suite/success/RefineInstance.v b/test-suite/success/RefineInstance.v
new file mode 100644
index 0000000000..f4d2f07db5
--- /dev/null
+++ b/test-suite/success/RefineInstance.v
@@ -0,0 +1,23 @@
+
+
+Class Foo := foo { a : nat; b : bool }.
+
+Fail Instance bla : Foo := { b:= true }.
+
+#[refine] Instance bla : Foo := { b:= true }.
+Proof.
+exact 0.
+Defined.
+
+Instance bli : Foo := { a:=1; b := false}.
+Check bli.
+
+Fail #[program, refine] Instance bla : Foo := {b := true}.
+
+#[program] Instance blo : Foo := {b := true}.
+Next Obligation. exact 2. Qed.
+Check blo.
+
+#[refine] Instance xbar : Foo := {a:=4; b:=true}.
+Proof. Qed.
+Check xbar.