blob: 39b4d2ab34fe5a05e6d7ad2b577333337734a54c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
type loc = {
loc_start : Lexing.position;
loc_end : Lexing.position;
}
type code = { code : string }
type user_symbol =
| Ulist1 of user_symbol
| Ulist1sep of user_symbol * string
| Ulist0 of user_symbol
| Ulist0sep of user_symbol * string
| Uopt of user_symbol
| Uentry of string
| Uentryl of string * int
type token_data =
| TokNone
| TokName of string
type ext_token =
| ExtTerminal of string
| ExtNonTerminal of user_symbol * token_data
type tactic_rule = {
tac_toks : ext_token list;
tac_body : code;
}
type level = string
type position =
| First
| Last
| Before of level
| After of level
| Level of level
type assoc =
| LeftA
| RightA
| NonA
type gram_symbol =
| GSymbString of string
| GSymbQualid of string * level option
| GSymbParen of gram_symbol list
| GSymbProd of gram_prod list
and gram_prod = {
gprod_symbs : (string option * gram_symbol list) list;
gprod_body : code;
}
type gram_rule = {
grule_label : string option;
grule_assoc : assoc option;
grule_prods : gram_prod list;
}
type grammar_entry = {
gentry_name : string;
gentry_pos : position option;
gentry_rules : gram_rule list;
}
type grammar_ext = {
gramext_name : string;
gramext_globals : string list;
gramext_entries : grammar_entry list;
}
type tactic_ext = {
tacext_name : string;
tacext_level : int option;
tacext_rules : tactic_rule list;
}
type node =
| Code of code
| Comment of string
| DeclarePlugin of string
| GramExt of grammar_ext
| VernacExt
| TacticExt of tactic_ext
type t = node list
|
