diff options
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 fb103b7823..1880a63a5d 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 cc960a267a..4ad165a4c7 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 |