summaryrefslogtreecommitdiff
path: root/math/coq
diff options
context:
space:
mode:
authorJohan van Selst <johans@FreeBSD.org>2010-12-10 17:23:11 +0000
committerJohan van Selst <johans@FreeBSD.org>2010-12-10 17:23:11 +0000
commit1daff35100a4b36ac837dd90575a12e6db9ecc6a (patch)
tree878bc30256a2e74b79909103f09999a552f876bc /math/coq
parentChange pre-install to pre-install-su to allow non-root to perform (diff)
Fix build with new ocaml preprocessor (patch from upstream)
Reported by: pointyhat via pav
Notes
Notes: svn path=/head/; revision=265995
Diffstat (limited to 'math/coq')
-rw-r--r--math/coq/Makefile1
-rw-r--r--math/coq/files/patch-camlp5-6-compat77
2 files changed, 78 insertions, 0 deletions
diff --git a/math/coq/Makefile b/math/coq/Makefile
index 158899528c8c..0a0dc93bade4 100644
--- a/math/coq/Makefile
+++ b/math/coq/Makefile
@@ -26,6 +26,7 @@ HAS_CONFIGURE= yes
CONFIGURE_ARGS= --prefix ${PREFIX}
CONFIGURE_ARGS+=--emacslib ${PREFIX}/share/emacs/site-lisp
CONFIGURE_ARGS+=--opt
+PATCH_STRIP= -p1
.ifdef NOPORTDOCS
CONFIGURE_ARGS+=--with-doc none
diff --git a/math/coq/files/patch-camlp5-6-compat b/math/coq/files/patch-camlp5-6-compat
new file mode 100644
index 000000000000..50ae78340dbc
--- /dev/null
+++ b/math/coq/files/patch-camlp5-6-compat
@@ -0,0 +1,77 @@
+From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
+Date: Tue, 16 Nov 2010 20:25:56 +0000 (+0000)
+Subject: Support for camlp5 6.02.0 (Closes: #2432)
+X-Git-Url: https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq%2Fcoq-svn.git;a=commitdiff_plain;h=501c9cb6ff7c903974123284fe795cdcaab8f300
+
+Support for camlp5 6.02.0 (Closes: #2432)
+
+git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@13641 85f007b7-540e-0410-9357-904b9bb8a0f7
+---
+
+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 4719e6d..5d37f4a 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