diff options
| author | Gaëtan Gilbert | 2019-05-16 16:49:03 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-21 12:44:30 +0200 |
| commit | f80f7c49cc9fb40b493be5cad787bd4b8f8fb717 (patch) | |
| tree | 54dde1d9352e99afce16755199f9331bfb758ea0 /stm | |
| parent | 02d6f5660d54fcf4dfc9cff36cbda41dca3f601f (diff) | |
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.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 2 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 4 |
2 files changed, 3 insertions, 3 deletions
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 |