mirror/freebsd-ports
1
0
Fork 0
mirror of https://git.FreeBSD.org/ports.git synced 2024-10-19 19:59:43 +00:00
Code Issues Releases Activity

- Update coq to 8.3pl1

Browse Source 
- Remove obsoleted patch (fixed in dist)
This commit is contained in:
Johan van Selst 2011-02-12 12:30:08 +00:00
parent 50ca2d54ed
commit 1bcf11304d
Notes: svn2git 2021-03-31 03:12:20 +00:00 
svn path=/head/; revision=268981
3 changed files with 3 additions and 80 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
math/coq/Makefile
View File

@ -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/ \

4
math/coq/distinfo
View File

@ -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

77
math/coq/files/patch-camlp5-6-compat
View File

@ -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