diff options
Diffstat (limited to 'library/misctypes.ml')
| -rw-r--r-- | library/misctypes.ml | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/library/misctypes.ml b/library/misctypes.ml index a12caef80..3b629f449 100644 --- a/library/misctypes.ml +++ b/library/misctypes.ml @@ -10,18 +10,6 @@ open Names -(** Basic types used both in [constr_expr], [glob_constr], and [vernacexpr] *) - -(** Located identifiers and objects with syntax. *) - -type lident = Id.t CAst.t -type lname = Name.t CAst.t -type lstring = string CAst.t - -(** Cases pattern variables *) - -type patvar = Id.t - (** Introduction patterns *) type 'constr intro_pattern_expr = |