diff options
| author | Pierre-Marie Pédrot | 2016-03-19 01:43:29 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-19 02:49:03 +0100 |
| commit | ce2ffd090bd64963279cbbb84012d1b266ed9918 (patch) | |
| tree | 842afc28f891fa8516cbb86d1051b41686eb67a6 /stm | |
| parent | 65e0522033ea47ed479227be30a92fceaa8c6358 (diff) | |
Moving VernacSolve to an EXTEND-based definition.
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 |