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.

9 files changed, 47 insertions, 91 deletions

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
        }
diff --git a/stm/stm.ml b/stm/stm.ml
index 21618bc044..6f7cefb582 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -364,7 +364,6 @@ module VCS : sig
   val set_parsing_state : id -> Vernacstate.Parser.state -> unit
   val get_parsing_state : id -> Vernacstate.Parser.state option
   val get_proof_mode : id -> Pvernac.proof_mode option
-  val set_proof_mode : id -> Pvernac.proof_mode option -> unit
 
   (* cuts from start -> stop, raising Expired if some nodes are not there *)
   val slice : block_start:id -> block_stop:id -> vcs
@@ -572,6 +571,7 @@ end = struct (* {{{ *)
     (match Vernacprop.under_control x with
     | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i
     | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i
+    | VernacInstance (_,(({CAst.v=Name i},_),_,_),_,_) -> Id.to_string i
     | _ -> "branch")
   let edit_branch = Branch.make "edit"
   let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
@@ -611,7 +611,6 @@ end = struct (* {{{ *)
     info.state <- new_state
 
   let get_proof_mode id = (get_info id).proof_mode
-  let set_proof_mode id pm = (get_info id).proof_mode <- pm
 
   let reached id =
     let info = get_info id in
@@ -3050,53 +3049,6 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
               VCS.set_parsing_state id parsing_state) new_ids;
           `Ok
 
-      (* Unknown: we execute it, check for open goals and propagate sideeff *)
-      | VtUnknown, VtNow ->
-          let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
-          if not (get_allow_nested_proofs ()) && in_proof then
-            "Commands which may open proofs are not allowed in a proof unless you turn option Nested Proofs Allowed on."
-            |> Pp.str
-            |> (fun s -> (UserError (None, s), Exninfo.null))
-            |> State.exn_on ~valid:Stateid.dummy newtip
-            |> Exninfo.iraise
-          else
-            let id = VCS.new_node ~id:newtip proof_mode () in
-          let head_id = VCS.get_branch_pos head in
-          let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *)
-          let step () =
-            VCS.checkout VCS.Branch.master;
-            let mid = VCS.get_branch_pos VCS.Branch.master in
-            let _st' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid in
-            let st = Vernacstate.freeze_interp_state ~marshallable:false in
-            ignore(stm_vernac_interp id st x);
-            (* Vernac x may or may not start a proof *)
-            if not in_proof && PG_compat.there_are_pending_proofs () then
-            begin
-              let bname = VCS.mk_branch_name x in
-              let opacity_of_produced_term = function
-                (* This AST is ambiguous, hence we check it dynamically *)
-                | VernacInstance (_,_ , None, _) -> GuaranteesOpacity
-                | _ -> Doesn'tGuaranteeOpacity in
-              VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[]));
-              VCS.set_proof_mode id (Some (Vernacentries.get_default_proof_mode ()));
-              VCS.branch bname (`Proof (VCS.proof_nesting () + 1));
-            end else begin
-              begin match (VCS.get_branch head).VCS.kind with
-              | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
-              | `Master -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
-              | `Proof _ ->
-                  VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
-                  (* We hope it can be replayed, but we can't really know *)
-                  ignore(VCS.propagate_sideff ~action:(ReplayCommand x));
-              end;
-              VCS.checkout_shallowest_proof_branch ();
-            end in
-          State.define ~doc ~safe_id:head_id ~cache:true step id;
-          Backtrack.record (); `Ok
-
-      | VtUnknown, VtLater ->
-          anomaly(str"classifier: VtUnknown must imply VtNow.")
-
       | VtProofMode pm, VtNow ->
         let proof_mode = Pvernac.lookup_proof_mode pm in
         let id = VCS.new_node ~id:newtip proof_mode () in
@@ -3106,7 +3058,6 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
 
       | VtProofMode _, VtLater ->
           anomaly(str"classifier: VtProofMode must imply VtNow.")
-
     end in
     let pr_rc rc = match rc with
       | `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"])
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 4a4c5c94e9..7cecd801e4 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -21,7 +21,6 @@ let string_of_parallel = function
   | `No -> ""
 
 let string_of_vernac_type = function
-  | VtUnknown -> "Unknown"
   | VtStartProof _ -> "StartProof"
   | VtSideff _ -> "Sideff"
   | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)"
@@ -61,7 +60,7 @@ let options_affecting_stm_scheduling =
   ]
 
 let classify_vernac e =
-  let static_classifier ~poly e = match e with
+  let static_classifier ~atts e = match e with
     (* Univ poly compatibility: we run it now, so that we can just
      * look at Flags in stm.ml.  Would be nicer to have the stm
      * look at the entire dag to detect this option. *)
@@ -97,15 +96,18 @@ let classify_vernac e =
       VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
 
     | VernacDefinition (_,({v=i},_),ProveBody _) ->
-       let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-        VtStartProof(guarantee, idents_of_name i), VtLater
+      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+      let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+      VtStartProof(guarantee, idents_of_name i), VtLater
     | VernacStartTheoremProof (_,l) ->
-        let ids = List.map (fun (({v=i}, _), _) -> i) l in
-       let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-        VtStartProof (guarantee,ids), VtLater
+      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+      let ids = List.map (fun (({v=i}, _), _) -> i) l in
+      let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+      VtStartProof (guarantee,ids), VtLater
     | VernacFixpoint (discharge,l) ->
+      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
        let guarantee =
-         if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+         if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
          else GuaranteesOpacity
        in
         let ids, open_proof =
@@ -115,8 +117,9 @@ let classify_vernac e =
         then VtStartProof (guarantee,ids), VtLater
         else VtSideff ids, VtLater
     | VernacCoFixpoint (discharge,l) ->
+      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
        let guarantee =
-         if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+         if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
          else GuaranteesOpacity
        in
         let ids, open_proof =
@@ -185,8 +188,12 @@ let classify_vernac e =
     | VernacDeclareMLModule _
     | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow
     | VernacProofMode pm -> VtProofMode pm, VtNow
-    (* These are ambiguous *)
-    | VernacInstance _ -> VtUnknown, VtNow
+    | 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), VtLater
+    | VernacInstance (_,((name,_),_,_),_,_) ->
+      VtSideff (idents_of_name name.CAst.v), VtLater
     (* Stm will install a new classifier to handle these *)
     | VernacBack _ | VernacAbortAll
     | VernacUndoTo _ | VernacUndo _
@@ -201,9 +208,8 @@ let classify_vernac e =
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
   in
   let rec static_control_classifier v = v |> CAst.with_val (function
-    | VernacExpr (f, e) ->
-      let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in
-      static_classifier ~poly e
+    | VernacExpr (atts, e) ->
+      static_classifier ~atts e
     | VernacTimeout (_,e) -> static_control_classifier e
     | VernacTime (_,e) | VernacRedirect (_, e) ->
        static_control_classifier e
@@ -214,6 +220,6 @@ let classify_vernac e =
         | VtQed _, _ ->
             VtProofStep { parallel = `No; proof_block_detection = None },
             VtLater
-        | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater))
+        | (VtStartProof _ | VtProofMode _), _ -> VtQuery, VtLater))
   in
   static_control_classifier e
diff --git a/test-suite/bugs/closed/bug_3890.v b/test-suite/bugs/closed/bug_3890.v
new file mode 100644
index 0000000000..e1823ac54c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_3890.v
@@ -0,0 +1,12 @@
+Set Nested Proofs Allowed.
+
+Class Foo.
+Class Bar := b : Type.
+
+Instance foo : Foo.
+
+Instance bar : Bar.
+exact Type.
+Defined.
+
+Defined.
diff --git a/test-suite/bugs/closed/bug_4580.v b/test-suite/bugs/closed/bug_4580.v
index a8a446cc9b..3f40569d61 100644
--- a/test-suite/bugs/closed/bug_4580.v
+++ b/test-suite/bugs/closed/bug_4580.v
@@ -2,6 +2,5 @@ Require Import Program.
 
 Class Foo (A : Type) := foo : A.
 
-Unset Refine Instance Mode.
 Program Instance f1 : Foo nat := S _.
 Next Obligation. exact 0. Defined.
diff --git a/test-suite/bugs/closed/bug_4638.v b/test-suite/bugs/closed/bug_4638.v
new file mode 100644
index 0000000000..951fe5302b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4638.v
@@ -0,0 +1,12 @@
+Set Nested Proofs Allowed.
+
+Class Foo.
+
+Goal True.
+
+Instance foo: Foo.
+Qed.
+
+trivial.
+
+Qed.
diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v
deleted file mode 100644
index 9d83743b2a..0000000000
--- a/test-suite/bugs/opened/bug_3890.v
+++ /dev/null
@@ -1,22 +0,0 @@
-Set Nested Proofs Allowed.
-
-Class Foo.
-Class Bar := b : Type.
-
-Set Refine Instance Mode.
-Instance foo : Foo := _.
-Unset Refine Instance Mode.
-(* 1 subgoals, subgoal 1 (ID 4)
-
-  ============================
-   Foo *)
-
-Instance bar : Bar.
-exact Type.
-Defined.
-(* bar is defined *)
-
-About foo.
-(* foo not a defined object. *)
-
-Fail Defined.
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 =