From a6757b089e1d268517bcba48a9fe33aa47526de2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 25 Jan 2019 00:06:32 +0100
Subject: Remove Refine Instance Mode option

---
 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 a68efa4713..963b7189f9 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1800,7 +1800,7 @@ let anew_instance ~pstate atts binders instance fields =
   let program_mode = atts.program in
   new_instance ~pstate ~program_mode atts.polymorphic
     binders instance (Some (true, CAst.make @@ CRecord (fields)))
-    ~global:atts.global ~generalize:false ~refine:false Hints.empty_hint_info
+    ~global:atts.global ~generalize:false Hints.empty_hint_info
 
 let declare_instance_refl ~pstate atts binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
-- 
cgit v1.2.3


From c352873936db93c251c544383853474736f128d6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 25 Jan 2019 00:48:36 +0100
Subject: Remove VtUnknown classification

This clean-up removes the dependency of the current proof mode (and hence
the parsing state) on unification.

The current proof mode can now be known simply by parsing and elaborating
attributes. We give access to attributes from the classifier for this purpose.

We remove the infamous `VtUnknown` code path in the STM which is known to
be buggy.

Fixes #3632 #3890 #4638.
---
 plugins/ltac/g_rewrite.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 469551809c..12b12bc7b0 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -278,7 +278,7 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
      }
   | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
     (* This command may or may not open a goal *)
-    => { VtUnknown, VtNow }
+    => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater }
     -> {
           add_morphism_infer atts m n
        }
-- 
cgit v1.2.3