diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 7 |
2 files changed, 9 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 6dae6ee23..359323902 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -103,9 +103,9 @@ GEXTEND Gram | b = bullet; tac = subgoal_command -> tac None (Some b)] ] ; bullet: - [ [ "-" -> Dash - | "*" -> Star - | "+" -> Plus ] ] + [ [ "-" -> Proof_global.Bullet.Dash + | "*" -> Proof_global.Bullet.Star + | "+" -> Proof_global.Bullet.Plus ] ] ; subgoal_command: [ [ c = check_command; "." -> fun g _ -> c g diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 4bf6e59f1..ebd8175d7 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -745,7 +745,12 @@ let rec pr_vernac = function (* Solving *) | VernacSolve (i,b,tac,deftac) -> (if i = 1 then mt() else int i ++ str ": ") ++ - (match b with None -> mt () | Some Dash -> str"-" | Some Star -> str"*" | Some Plus -> str"+") ++ + begin match b with + | None -> mt () + | Some Proof_global.Bullet.Dash -> str"-" + | Some Proof_global.Bullet.Star -> str"*" + | Some Proof_global.Bullet.Plus -> str"+" + end ++ pr_raw_tactic tac ++ (try if deftac then str ".." else mt () with UserError _|Loc.Exc_located _ -> mt()) |