diff options
Diffstat (limited to 'debian/patches/0003-Support-for-camlp5-6.02.1.patch')
| -rw-r--r-- | debian/patches/0003-Support-for-camlp5-6.02.1.patch | 156 |
1 files changed, 156 insertions, 0 deletions
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 00000000..4dfaa7b9 --- /dev/null +++ b/debian/patches/0003-Support-for-camlp5-6.02.1.patch @@ -0,0 +1,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." + + (**********************************************************************) +-- |