diff options
author | 2015-02-15 18:35:32 +0100 | |
---|---|---|
committer | 2015-02-15 19:03:42 +0100 | |
commit | 1c46875f39756e1bd12c5d6009391a2b5927826f (patch) | |
tree | 3966094a5f91fc8ddab5328ded063b09e7d6e529 /stm/vernac_classifier.ml | |
parent | aed3c876d422f4dcc0296fd4949148c697f37b1d (diff) |
Reset "section name" works again (Close #3933)
Diffstat (limited to 'stm/vernac_classifier.ml')
-rw-r--r-- | stm/vernac_classifier.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index e9302bb73..81fad1379 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -151,8 +151,8 @@ let rec classify_vernac e = let ids = List.map snd (CList.map_filter (fun (x,_) -> x) l) in VtSideff ids, VtLater | VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater + | VernacBeginSection (_,id) -> VtSideff [id], VtLater | VernacUniverse _ | VernacConstraint _ - | VernacBeginSection _ | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _ | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ | VernacChdir _ |