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

---
 vernac/classes.ml  | 18 ++++--------------
 vernac/classes.mli |  1 -
 2 files changed, 4 insertions(+), 15 deletions(-)

(limited to 'vernac')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index ece9fc8937..05a75ab435 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -31,16 +31,6 @@ module NamedDecl = Context.Named.Declaration
 open Decl_kinds
 open Entries
 
-let refine_instance = ref false
-
-let () = Goptions.(declare_bool_option {
-  optdepr  = true;
-  optname  = "definition of instances by refining";
-  optkey   = ["Refine";"Instance";"Mode"];
-  optread  = (fun () -> !refine_instance);
-  optwrite = (fun b -> refine_instance := b)
-})
-
 let set_typeclass_transparency c local b = 
   Hints.add_hints ~local [typeclasses_db]
     (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b))
@@ -419,7 +409,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po
         | None ->
           pstate) ())
 
-let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
+let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
   let props =
     match props with
     | Some (true, { CAst.v = CRecord fs }) ->
@@ -503,7 +493,7 @@ let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program
       let term = to_constr sigma (Option.get term) in
       (declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype;
        None)
-    else if program_mode || refine || Option.is_empty props then
+    else if program_mode || Option.is_empty props then
       declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype
     else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in
   id, pstate
@@ -550,7 +540,7 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl =
   sigma, cl, u, c', ctx', ctx, imps, args, decl
 
 
-let new_instance ~pstate ?(global=false) ?(refine= !refine_instance) ~program_mode
+let new_instance ~pstate ?(global=false) ~program_mode
     poly ctx (instid, bk, cl) props
     ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
@@ -566,7 +556,7 @@ let new_instance ~pstate ?(global=false) ?(refine= !refine_instance) ~program_mo
       Namegen.next_global_ident_away i (Termops.vars_of_env env)
   in
   let env' = push_rel_context ctx env in
-  do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode
+  do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode
     cty k u ctx ctx' pri decl imps subst id props
 
 let declare_new_instance ?(global=false) ~program_mode poly ctx (instid, bk, cl) pri =
diff --git a/vernac/classes.mli b/vernac/classes.mli
index e7f90ff306..57bb9ce312 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -48,7 +48,6 @@ val declare_instance_constant :
 val new_instance :
   pstate:Proof_global.t option ->
   ?global:bool (** Not global by default. *) ->
-  ?refine:bool (** Allow refinement *) ->
   program_mode:bool ->
   Decl_kinds.polymorphic ->
   local_binder_expr list ->
-- 
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.
---
 vernac/vernacextend.ml  | 1 -
 vernac/vernacextend.mli | 1 -
 2 files changed, 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index ef06e59316..730f5fd6da 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -36,7 +36,6 @@ type vernac_type =
   | VtProofMode of string
   (* To be removed *)
   | VtMeta
-  | VtUnknown
 and vernac_start = opacity_guarantee * Names.Id.t list
 and vernac_sideff_type = Names.Id.t list
 and opacity_guarantee =
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 4d89eaffd9..54e08d0e95 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -52,7 +52,6 @@ type vernac_type =
   | VtProofMode of string
   (* To be removed *)
   | VtMeta
-  | VtUnknown
 and vernac_start = opacity_guarantee * Names.Id.t list
 and vernac_sideff_type = Names.Id.t list
 and opacity_guarantee =
-- 
cgit v1.2.3