From 584a832d4f681d34c7cbdd87d9ceb7a742b39959 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 Feb 2017 00:23:10 +0100 Subject: [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. --- vernac/vernacentries.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'vernac') 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) -> -- cgit v1.2.3