From f80f7c49cc9fb40b493be5cad787bd4b8f8fb717 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 16 May 2019 16:49:03 +0200
Subject: Remove undocumented Instance : ! syntax

It's used a few times in the stdlib (a couple of which need no other
change when removing the !) and not at all throughout our CI.

Considering that I think it's fair enough to remove it.
---
 stm/stm.ml               | 2 +-
 stm/vernac_classifier.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 6f7cefb582..29acb77af2 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -571,7 +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
+    | 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
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 7cecd801e4..aa16f9535d 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -188,11 +188,11 @@ let classify_vernac e =
     | VernacDeclareMLModule _
     | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow
     | VernacProofMode pm -> VtProofMode pm, VtNow
-    | VernacInstance (_,((name,_),_,_),None,_) when not (Attributes.parse_drop_extra Attributes.program atts) ->
+    | 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,_),_,_),_,_) ->
+    | VernacInstance ((name,_),_,_,_,_) ->
       VtSideff (idents_of_name name.CAst.v), VtLater
     (* Stm will install a new classifier to handle these *)
     | VernacBack _ | VernacAbortAll
-- 
cgit v1.2.3