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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
|
From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 16 Nov 2010 20:25:56 +0000
Subject: [PATCH] Support for camlp5 6.02.1
Signed-off-by: Stephane Glondu <steph@glondu.net>
---
lib/compat.ml4 | 12 ++++++++++++
parsing/pcoq.ml4 | 23 ++++++++++++++---------
parsing/pcoq.mli | 2 ++
toplevel/metasyntax.ml | 26 +++++++++++++-------------
4 files changed, 41 insertions(+), 22 deletions(-)
diff --git a/lib/compat.ml4 b/lib/compat.ml4
index 9b6bb19..a77c2bc 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -65,3 +65,15 @@ let unloc = M.unloc
let join_loc = M.join_loc
type token = M.token
type lexer = M.lexer
+
+IFDEF CAMLP5_6_00 THEN
+
+let slist0sep x y = Gramext.Slist0sep (x, y, false)
+let slist1sep x y = Gramext.Slist1sep (x, y, false)
+
+ELSE
+
+let slist0sep x y = Gramext.Slist0sep (x, y)
+let slist1sep x y = Gramext.Slist1sep (x, y)
+
+END
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 90a9220..de1b3ed 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -145,6 +145,11 @@ module Gram =
G.delete_rule e pil
end
+IFDEF CAMLP5_6_02_1 THEN
+let entry_print x = Gram.Entry.print !Pp_control.std_ft x
+ELSE
+let entry_print = Gram.Entry.print
+END
let camlp4_verbosity silent f x =
let a = !Gramext.warning_verbose in
@@ -631,16 +636,16 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
| ETConstrList (typ',[]) ->
Gramext.Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
| ETConstrList (typ',tkl) ->
- Gramext.Slist1sep
- (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'),
- make_sep_rules tkl)
+ Compat.slist1sep
+ (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
+ (make_sep_rules tkl)
| ETBinderList (false,[]) ->
Gramext.Slist1
(symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
| ETBinderList (false,tkl) ->
- Gramext.Slist1sep
- (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false),
- make_sep_rules tkl)
+ Compat.slist1sep
+ (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
+ (make_sep_rules tkl)
| _ ->
match interp_constr_prod_entry_key assoc from forpat typ with
| (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj)
@@ -654,16 +659,16 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
let rec symbol_of_prod_entry_key = function
| Alist1 s -> Gramext.Slist1 (symbol_of_prod_entry_key s)
| Alist1sep (s,sep) ->
- Gramext.Slist1sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep))
+ Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep))
| Alist0 s -> Gramext.Slist0 (symbol_of_prod_entry_key s)
| Alist0sep (s,sep) ->
- Gramext.Slist0sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep))
+ Compat.slist0sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep))
| Aopt s -> Gramext.Sopt (symbol_of_prod_entry_key s)
| Amodifiers s ->
Gramext.srules
[([], Gramext.action(fun _loc -> []));
([Gramext.Stoken ("", "(");
- Gramext.Slist1sep ((symbol_of_prod_entry_key s), Gramext.Stoken ("", ","));
+ Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", ","));
Gramext.Stoken ("", ")")],
Gramext.action (fun _ l _ _loc -> l))]
| Aself -> Gramext.Sself
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e4566e7..7dbd78e 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -23,6 +23,8 @@ open Libnames
module Gram : Grammar.S with type te = Compat.token
+val entry_print : 'a Gram.Entry.e -> unit
+
(**********************************************************************)
(* The parser of Coq is built from three kinds of rule declarations:
- dynamic rules declared at the evaluation of Coq files (using
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6ee00f4..ddb1b11 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -106,33 +106,33 @@ let add_tactic_notation (n,prods,e) =
let print_grammar = function
| "constr" | "operconstr" | "binder_constr" ->
msgnl (str "Entry constr is");
- Gram.Entry.print Pcoq.Constr.constr;
+ entry_print Pcoq.Constr.constr;
msgnl (str "and lconstr is");
- Gram.Entry.print Pcoq.Constr.lconstr;
+ entry_print Pcoq.Constr.lconstr;
msgnl (str "where binder_constr is");
- Gram.Entry.print Pcoq.Constr.binder_constr;
+ entry_print Pcoq.Constr.binder_constr;
msgnl (str "and operconstr is");
- Gram.Entry.print Pcoq.Constr.operconstr;
+ entry_print Pcoq.Constr.operconstr;
| "pattern" ->
- Gram.Entry.print Pcoq.Constr.pattern
+ entry_print Pcoq.Constr.pattern
| "tactic" ->
msgnl (str "Entry tactic_expr is");
- Gram.Entry.print Pcoq.Tactic.tactic_expr;
+ entry_print Pcoq.Tactic.tactic_expr;
msgnl (str "Entry binder_tactic is");
- Gram.Entry.print Pcoq.Tactic.binder_tactic;
+ entry_print Pcoq.Tactic.binder_tactic;
msgnl (str "Entry simple_tactic is");
- Gram.Entry.print Pcoq.Tactic.simple_tactic;
+ entry_print Pcoq.Tactic.simple_tactic;
| "vernac" ->
msgnl (str "Entry vernac is");
- Gram.Entry.print Pcoq.Vernac_.vernac;
+ entry_print Pcoq.Vernac_.vernac;
msgnl (str "Entry command is");
- Gram.Entry.print Pcoq.Vernac_.command;
+ entry_print Pcoq.Vernac_.command;
msgnl (str "Entry syntax is");
- Gram.Entry.print Pcoq.Vernac_.syntax;
+ entry_print Pcoq.Vernac_.syntax;
msgnl (str "Entry gallina is");
- Gram.Entry.print Pcoq.Vernac_.gallina;
+ entry_print Pcoq.Vernac_.gallina;
msgnl (str "Entry gallina_ext is");
- Gram.Entry.print Pcoq.Vernac_.gallina_ext;
+ entry_print Pcoq.Vernac_.gallina_ext;
| _ -> error "Unknown or unprintable grammar entry."
(**********************************************************************)
--
|
