diff options
| author | Vincent Laporte | 2019-05-23 07:23:22 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-05-23 07:23:22 +0000 |
| commit | a559c7b6de7854f46ed42869c6100f3751d36ade (patch) | |
| tree | a1d0f5e7e631c524e87fbff4f4561da7778fe221 /stm | |
| parent | 4663542d9410d1bd0e074a493e1f04686e00dd8b (diff) | |
| parent | 052ade5cfa57763fa48ae273e1a6369552bfb918 (diff) | |
Merge PR #10185: Remove undocumented Instance : ! syntax
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: vbgl
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 10f4865dfd..fc539b5208 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -580,7 +580,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 |