diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/texmacspp.ml | 2 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
2 files changed, 1 insertions, 3 deletions
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 3c4b8cb71e..a459cd65f8 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -671,7 +671,7 @@ let rec tmpp v loc = (* Solving *) - | (VernacSolve _ | VernacSolveExistential _) as x -> + | (VernacSolveExistential _) as x -> xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] (* Auxiliary file and library management *) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f9f08f7afb..97d6e1fb71 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -102,12 +102,10 @@ let rec classify_vernac e = | VernacCheckMayEval _ -> VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater (* ProofStep *) - | VernacSolve (SelectAllParallel,_,_,_) -> VtProofStep true, VtLater | VernacProof _ | VernacBullet _ | VernacFocus _ | VernacUnfocus | VernacSubproof _ | VernacEndSubproof - | VernacSolve _ | VernacCheckGuard | VernacUnfocused | VernacSolveExistential _ -> VtProofStep false, VtLater |