diff options
| author | Pierre-Marie Pédrot | 2016-09-15 19:21:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-15 19:35:28 +0200 |
| commit | 6f123367027055dbefd9aec9ab2a8bc62f6c32ed (patch) | |
| tree | 150d49dde41052019d8728dee924d9d679b51161 /ltac | |
| parent | 72ac4b32ac26fdba751ae48568d28b4dbb8edd14 (diff) | |
Made Ppanotation Ltac-agnostic.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/pptactic.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml index dc2676bf4b..271ed12d52 100644 --- a/ltac/pptactic.ml +++ b/ltac/pptactic.ml @@ -1329,16 +1329,17 @@ module Richpp = struct include Make (Ppconstr.Richpp) (struct open Ppannotation + open Genarg let do_not_tag _ x = x let tag e s = Pp.tag (Pp.Tag.inj e tag) s let tag_keyword = tag AKeyword let tag_primitive = tag AKeyword let tag_string = do_not_tag () - let tag_glob_tactic_expr e = tag (AGlobTacticExpr e) - let tag_glob_atomic_tactic_expr a = tag (AGlobAtomicTacticExpr a) - let tag_raw_tactic_expr e = tag (ARawTacticExpr e) - let tag_raw_atomic_tactic_expr a = tag (ARawAtomicTacticExpr a) - let tag_atomic_tactic_expr a = tag (AAtomicTacticExpr a) + let tag_glob_tactic_expr e = tag (AGlbGenArg (in_gen (glbwit wit_ltac) e)) + let tag_glob_atomic_tactic_expr = do_not_tag + let tag_raw_tactic_expr e = tag (ARawGenArg (in_gen (rawwit wit_ltac) e)) + let tag_raw_atomic_tactic_expr = do_not_tag + let tag_atomic_tactic_expr = do_not_tag end) end |