diff options
Diffstat (limited to 'printing/ppannotation.mli')
| -rw-r--r-- | printing/ppannotation.mli | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli index d10bc5a571..9e3ab2b0e2 100644 --- a/printing/ppannotation.mli +++ b/printing/ppannotation.mli @@ -12,12 +12,19 @@ open Ppextend open Constrexpr open Vernacexpr +open Tacexpr type t = | AKeyword - | AUnparsing of unparsing - | AConstrExpr of constr_expr - | AVernac of vernac_expr + | AUnparsing of unparsing + | AConstrExpr of constr_expr + | AVernac of vernac_expr + | AGlobTacticExpr of glob_tactic_expr + | AGlobAtomicTacticExpr of glob_atomic_tactic_expr + | ARawTacticExpr of raw_tactic_expr + | ARawAtomicTacticExpr of raw_atomic_tactic_expr + | ATacticExpr of tactic_expr + | AAtomicTacticExpr of atomic_tactic_expr val tag_of_annotation : t -> string |