diff options
Diffstat (limited to 'printing/ppannotation.mli')
| -rw-r--r-- | printing/ppannotation.mli | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli index a0fef1a75..b0e0facef 100644 --- a/printing/ppannotation.mli +++ b/printing/ppannotation.mli @@ -12,18 +12,15 @@ open Ppextend open Constrexpr open Vernacexpr -open Tacexpr +open Genarg type t = | AKeyword | 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 - | AAtomicTacticExpr of atomic_tactic_expr + | AGlbGenArg of glob_generic_argument + | ARawGenArg of raw_generic_argument val tag_of_annotation : t -> string |