[Pkg-ocaml-maint-commits] [SCM] coq packaging branch, experimental/master, updated. debian/8.3.rc1+dfsg-1-14-gc0a9252
Stephane Glondu
steph at glondu.net
Mon Dec 6 12:47:36 UTC 2010
The following commit has been merged in the experimental/master branch:
commit c0a92523eaa76afabcbaf06ac4a7e8f7930ee4a3
Author: Stephane Glondu <steph at glondu.net>
Date: Mon Dec 6 11:24:02 2010 +0100
Port to camlp5 6.02.1
diff --git a/debian/patches/0003-Support-for-camlp5-6.02.0.patch b/debian/patches/0003-Support-for-camlp5-6.02.0.patch
deleted file mode 100644
index 5ed3f54..0000000
--- a/debian/patches/0003-Support-for-camlp5-6.02.0.patch
+++ /dev/null
@@ -1,78 +0,0 @@
-From: glondu <glondu at 85f007b7-540e-0410-9357-904b9bb8a0f7>
-Date: Tue, 16 Nov 2010 20:25:56 +0000
-Subject: [PATCH] Support for camlp5 6.02.0
-
-Signed-off-by: Stephane Glondu <steph at glondu.net>
----
- lib/compat.ml4 | 12 ++++++++++++
- parsing/pcoq.ml4 | 18 +++++++++---------
- 2 files changed, 21 insertions(+), 9 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..9a1630f 100644
---- a/parsing/pcoq.ml4
-+++ b/parsing/pcoq.ml4
-@@ -631,16 +631,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 +654,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/debian/patches/0003-Support-for-camlp5-6.02.1.patch b/debian/patches/0003-Support-for-camlp5-6.02.1.patch
new file mode 100644
index 0000000..4dfaa7b
--- /dev/null
+++ b/debian/patches/0003-Support-for-camlp5-6.02.1.patch
@@ -0,0 +1,156 @@
+From: glondu <glondu at 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 at 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."
+
+ (**********************************************************************)
+--
diff --git a/debian/patches/series b/debian/patches/series
index d2da26e..de7a495 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,3 +1,3 @@
0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch
0002-Fix-mixed-implicit-and-normal-rules.patch
-0003-Support-for-camlp5-6.02.0.patch
+0003-Support-for-camlp5-6.02.1.patch
--
coq packaging
More information about the Pkg-ocaml-maint-commits
mailing list