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 /printing/ppvernac.ml | |
| parent | 65e0522033ea47ed479227be30a92fceaa8c6358 (diff) | |
Moving VernacSolve to an EXTEND-based definition.
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index a101540aba..887a14d2bf 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -979,24 +979,6 @@ module Make prlist_with_sep (fun () -> str " <+ ") pr_m mexprs) ) (* Solving *) - | VernacSolve (i,info,tac,deftac) -> - let pr_goal_selector = function - | SelectNth i -> int i ++ str":" - | SelectId id -> pr_id id ++ str":" - | SelectAll -> str"all" ++ str":" - | SelectAllParallel -> str"par" - in - let pr_info = - match info with - | None -> mt () - | Some i -> str"Info"++spc()++int i++spc() - in - return ( - (if i = Proof_global.get_default_goal_selector () then mt() else pr_goal_selector i) ++ - pr_info ++ - pr_raw_tactic tac - ++ (if deftac then str ".." else mt ()) - ) | VernacSolveExistential (i,c) -> return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c) |