3 files changed, 3 insertions, 80 deletions

diff --git a/math/coq/Makefile b/math/coq/Makefile
index 0a0dc93bade4..0b6fee6d859f 100644
--- a/math/coq/Makefile
+++ b/math/coq/Makefile
@@ -6,7 +6,7 @@
 #
 
 PORTNAME=	coq
-DISTVERSION=	8.3
+DISTVERSION=	8.3pl1
 PORTEPOCH=	1
 CATEGORIES=	math
 MASTER_SITES=	http://coq.inria.fr/distrib/V${DISTVERSION}/files/ \
diff --git a/math/coq/distinfo b/math/coq/distinfo
index ec25d1f8f8b8..baa7243797ef 100644
--- a/math/coq/distinfo
+++ b/math/coq/distinfo
@@ -1,2 +1,2 @@
-SHA256 (coq-8.3.tar.gz) = bd818e053948e6eed288753fe10fe2b23bdc6f277a8fe50a6233d8f07b263e0a
-SIZE (coq-8.3.tar.gz) = 3736420
+SHA256 (coq-8.3pl1.tar.gz) = 3a497386bd74f43a5af1d0c53f29a017ce7ed1b1e60c052217fe04b7f40be928
+SIZE (coq-8.3pl1.tar.gz) = 3756961
diff --git a/math/coq/files/patch-camlp5-6-compat b/math/coq/files/patch-camlp5-6-compat
deleted file mode 100644
index 50ae78340dbc..000000000000
--- a/math/coq/files/patch-camlp5-6-compat
+++ /dev/null
@@ -1,77 +0,0 @@
-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