diff options
| author | Regis-Gianas | 2014-11-04 14:46:47 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 22:51:36 +0100 |
| commit | db9b17d55f539fcfda799a9fe15caa2530cc727f (patch) | |
| tree | 112ce79b5bff93308caff927f138fd2768dde5be /printing/ppannotation.ml | |
| parent | 7b3f2d2783f74a38b4fe40d2dc5f58b8d5bae0f1 (diff) | |
printing/Ppannotation: Introduce a new annotation for keywords.
printing/{Ppconstr, Ppvernac}: Use it.
Diffstat (limited to 'printing/ppannotation.ml')
| -rw-r--r-- | printing/ppannotation.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml index b739dcaeb9..60d5da413b 100644 --- a/printing/ppannotation.ml +++ b/printing/ppannotation.ml @@ -11,11 +11,13 @@ open Constrexpr open Vernacexpr type t = + | AKeyword | AUnparsing of unparsing | AConstrExpr of constr_expr | AVernac of vernac_expr let tag_of_annotation = function + | AKeyword -> "keyword" | AUnparsing _ -> "unparsing" | AConstrExpr _ -> "constr_expr" | AVernac _ -> "vernac_expr" |