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.mli | |
| parent | 7b3f2d2783f74a38b4fe40d2dc5f58b8d5bae0f1 (diff) | |
printing/Ppannotation: Introduce a new annotation for keywords.
printing/{Ppconstr, Ppvernac}: Use it.
Diffstat (limited to 'printing/ppannotation.mli')
| -rw-r--r-- | printing/ppannotation.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli index 38b09eef0c..d10bc5a571 100644 --- a/printing/ppannotation.mli +++ b/printing/ppannotation.mli @@ -14,6 +14,7 @@ open Constrexpr open Vernacexpr type t = + | AKeyword | AUnparsing of unparsing | AConstrExpr of constr_expr | AVernac of vernac_expr |