diff options
| author | Enrico Tassi | 2015-02-15 18:35:32 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-02-15 19:03:42 +0100 |
| commit | 1c46875f39756e1bd12c5d6009391a2b5927826f (patch) | |
| tree | 3966094a5f91fc8ddab5328ded063b09e7d6e529 | |
| parent | aed3c876d422f4dcc0296fd4949148c697f37b1d (diff) | |
Reset "section name" works again (Close #3933)
| -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 e9302bb735..81fad13793 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 _ |