diff options
Diffstat (limited to 'printing/ppannotation.ml')
| -rw-r--r-- | printing/ppannotation.ml | 39 |
1 files changed, 0 insertions, 39 deletions
diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml deleted file mode 100644 index 511f9356..00000000 --- a/printing/ppannotation.ml +++ /dev/null @@ -1,39 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Ppextend -open Constrexpr -open Vernacexpr -open Tacexpr - -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 - -let tag_of_annotation = function - | AKeyword -> "keyword" - | AUnparsing _ -> "unparsing" - | AConstrExpr _ -> "constr_expr" - | AVernac _ -> "vernac_expr" - | AGlobTacticExpr _ -> "glob_tactic_expr" - | AGlobAtomicTacticExpr _ -> "glob_atomic_tactic_expr" - | ARawTacticExpr _ -> "raw_tactic_expr" - | ARawAtomicTacticExpr _ -> "raw_atomic_tactic_expr" - | AAtomicTacticExpr _ -> "atomic_tactic_expr" - -let attributes_of_annotation a = - [] - -let tag = Pp.Tag.create "ppannotation" |