1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
10
(*i $Id: extend.ml 7761 2005-12-30 10:52:19Z herbelin $ i*)
20
(**********************************************************************)
21
(* constr entry keys *)
23
type side = Left | Right
25
type production_position =
26
| BorderProd of side * Gramext.g_assoc option (* true=left; false=right *)
29
type production_level =
33
type ('lev,'pos) constr_entry_key =
34
| ETIdent | ETReference | ETBigint
35
| ETConstr of ('lev * 'pos)
37
| ETOther of string * string
38
| ETConstrList of ('lev * 'pos) * Token.pattern list
40
type constr_production_entry =
41
(production_level,production_position) constr_entry_key
43
(int,unit) constr_entry_key
44
type simple_constr_production_entry =
45
(production_level,unit) constr_entry_key
47
(**********************************************************************)
48
(* syntax modifiers *)
50
type syntax_modifier =
51
| SetItemLevel of string list * production_level
53
| SetAssoc of Gramext.g_assoc
54
| SetEntryType of string * simple_constr_production_entry
56
| SetFormat of string located