diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-18 16:35:46 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-18 17:08:07 +0100 |
| commit | b49d803286ba9ed711313702bb4269c5e9c516fa (patch) | |
| tree | 1f0c6407edb61f112c0872377ba2cef34386d554 /stm | |
| parent | fc3b70a11aff48eedd7b235f5732cd170a6ab8be (diff) | |
Proof using: New vernacular to name sets of section variables
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/texmacspp.ml | 1 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index fb103b782..1880a63a5 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -617,6 +617,7 @@ let rec tmpp v loc = (* Gallina extensions *) | VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id) | VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id) + | VernacNameSectionHypSet _ as x -> xmlTODO loc x | VernacRequire (None,l) -> xmlRequire loc (List.map (fun ref -> xmlReference ref) l) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index cc960a267..4ad165a4c 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -169,6 +169,7 @@ let rec classify_vernac e = | VernacDeclareClass _ | VernacDeclareInstances _ | VernacRegister _ | VernacDeclareTacticDefinition _ + | VernacNameSectionHypSet _ | VernacComments _ -> VtSideff [], VtLater (* Who knows *) | VernacLoad _ -> VtSideff [], VtNow |