diff options
| author |  courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-16 14:34:13 +0000 |
|---|---|---|
| committer | courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-16 14:34:13 +0000 |
| commit | 80ef72aa037175549f396e9618274ba69a81cf80 (patch) | |
| tree | f2b1c3e66f58c552eeac83e67216a89a96b56bff /parsing/ppvernac.ml | |
| parent | b076264235980e60d51a5d0b8d3a4e9c3f4d82eb (diff) | |
Moving bullets (-, +, *) into stand-alone commands instead of being
part of a tactic.
WARNING: Coqide needs to be adapted.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14794 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ppvernac.ml')
| -rw-r--r-- | parsing/ppvernac.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index e10d42b9d..c858439e6 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -754,14 +754,8 @@ let rec pr_vernac = function hov 2 (str"Include " ++ prlist_with_sep (fun () -> str " <+ ") pr_m mexprs) (* Solving *) - | VernacSolve (i,b,tac,deftac) -> + | VernacSolve (i,tac,deftac) -> (if i = 1 then mt() else int i ++ str ": ") ++ - begin match b with - | None -> mt () - | Some Dash -> str"-" - | Some Star -> str"*" - | Some Plus -> str"+" - end ++ pr_raw_tactic tac ++ (try if deftac then str ".." else mt () with UserError _|Loc.Exc_located _ -> mt()) @@ -979,6 +973,11 @@ let rec pr_vernac = function str "Proof using" ++spc()++ prlist pr_lident l ++ spc() ++ str "with" ++ spc() ++pr_raw_tactic te | VernacProofMode s -> str ("Proof Mode "^s) + | VernacBullet b -> begin match b with + | Dash -> str"-" + | Star -> str"*" + | Plus -> str"+" + end ++ spc() | VernacSubproof None -> str "BeginSubproof" | VernacSubproof (Some i) -> str "BeginSubproof " ++ pr_int i | VernacEndSubproof -> str "EndSubproof" |