diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-22 00:23:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-24 14:18:18 +0100 |
| commit | 584a832d4f681d34c7cbdd87d9ceb7a742b39959 (patch) | |
| tree | 1030c2c5a0a3dbfdb2b08773f2ca56ab80cde835 /vernac | |
| parent | 530cd175c1b7465c3fa35c300f42b022bed9b25b (diff) | |
[stm] Remove some obsolete vernacs/classification.
This is the good parts of PR #360.
IIUC, these vernacular were meant mostly for debugging and they are
not supposed to be of any use these days.
Back and join are still there not to break the testing infrastructure,
but some day they should go away.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 32e18a014..64c06d77a 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2210,6 +2210,11 @@ let with_fail b f = let interp ?(verbosely=true) ?proof (loc,c) = let orig_program_mode = Flags.is_program_mode () in let rec aux ?locality ?polymorphism isprogcmd = function + + (* This assert case will be removed when fake_ide can understand + completion feedback *) + | VernacStm _ -> assert false (* Done by Stm *) + | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c | VernacProgram _ -> CErrors.error "Program mode specified twice" | VernacLocal (b, c) when Option.is_empty locality -> @@ -2218,9 +2223,6 @@ let interp ?(verbosely=true) ?proof (loc,c) = aux ?locality ~polymorphism:b isprogcmd c | VernacPolymorphic (b, c) -> CErrors.error "Polymorphism specified twice" | VernacLocal _ -> CErrors.error "Locality specified twice" - | VernacStm (Command c) -> aux ?locality ?polymorphism isprogcmd c - | VernacStm (PGLast c) -> aux ?locality ?polymorphism isprogcmd c - | VernacStm _ -> assert false (* Done by Stm *) | VernacFail v -> with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v) | VernacTimeout (n,v) -> |