aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/vernac_classifier.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-02-15 18:35:32 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-02-15 19:03:42 +0100
commit1c46875f39756e1bd12c5d6009391a2b5927826f (patch)
tree3966094a5f91fc8ddab5328ded063b09e7d6e529 /stm/vernac_classifier.ml
parentaed3c876d422f4dcc0296fd4949148c697f37b1d (diff)
Reset "section name" works again (Close #3933)
Diffstat (limited to 'stm/vernac_classifier.ml')
-rw-r--r--stm/vernac_classifier.ml2
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 _