summaryrefslogtreecommitdiff
path: root/lang/coq
diff options
context:
space:
mode:
authortonio <tonio@pkgsrc.org>2009-09-05 20:44:57 +0000
committertonio <tonio@pkgsrc.org>2009-09-05 20:44:57 +0000
commit4c376968032b3da180096d3f4050977eff5cc845 (patch)
tree97cedfa48468d1c26c30cbc640af0572958adca1 /lang/coq
parentd24d2efda3ff543d042d5cffbf5543f340f38847 (diff)
downloadpkgsrc-4c376968032b3da180096d3f4050977eff5cc845.tar.gz
Update lang/coq to 8.2pl1
Changes from V8.1 to V8.2 ========================= Language - If a fixpoint is not written with an explicit { struct ... }, then all arguments are tried successively (from left to right) until one is found that satisfies the structural decreasing condition. - New experimental typeclass system giving ad-hoc polymorphism and overloading based on dependent records and implicit arguments. - New syntax "let 'pat := b in c" for let-binding using irrefutable patterns. - New syntax "forall {A}, T" for specifying maximally inserted implicit arguments in terms. - Sort of Record/Structure, Inductive and CoInductive defaults to Type if omitted. - Support for optional "where" notation clauses for record fields. - (Co)Inductive types can be defined as records (e.g. "CoInductive stream := { hd : nat; tl : stream }.") - New syntax "Theorem id1:t1 ... with idn:tn" for proving mutually dependent statements. - Support for sort-polymorphism on constants denoting inductive types. - Several evolutions of the module system (handling of module aliases, functorial module types, an Include feature, etc). - Prop now a subtype of Set (predicative and impredicative forms). - Recursive inductive types in Prop with a single constructor of which all arguments are in Prop is now considered to be a singleton type. It consequently supports all eliminations to Prop, Set and Type. As a consequence, Acc_rect has now a more direct proof [possible source of easily fixed incompatibility in case of manual definition of a recursor in a recursive singleton inductive type]. - New syntax to do implicit generalization in binders and inside terms. - New tentative syntax for introduction of record objects without mentioning the constructor {| field := body; ... |}, turning missing fields into holes (compatible with refine and Program). Vernacular commands - Added option Global to "Arguments Scope" for section surviving. - Added option "Unset Elimination Schemes" to deactivate the automatic generation of elimination schemes. - Modification of the Scheme command so you can ask for the name to be automatically computed (e.g. Scheme Induction for nat Sort Set). - New command "Combined Scheme" to build combined mutual induction principles from existing mutual induction principles. - New command "Scheme Equality" to build a decidable (boolean) equality for simple inductive datatypes and a decision property over this equality (e.g. Scheme Equality for nat). - Added option "Set Equality Scheme" to make automatic the declaration of the boolean equality when possible. - Source of universe inconsistencies now printed when option "Set Printing Universes" is activated. - New option "Set Printing Existential Instances" for making the display of existential variable instances explicit. - Support for option "[id1 ... idn]", and "-[id1 ... idn]", for the "compute"/"cbv" reduction strategy, respectively meaning reduce only, or everything but, the constants id1 ... idn. "lazy" alone or followed by "[id1 ... idn]", and "-[id1 ... idn]" also supported, meaning apply all of beta-iota-zeta-delta, possibly restricting delta. - New command "Strategy" to control the expansion of constants during conversion tests. It generalizes commands Opaque and Transparent by introducing a range of levels. Lower levels are assigned to constants that should be expanded first. - New options Global and Local to Opaque and Transparent. - New command "Print Assumptions" to display all variables, parameters or axioms a theorem or definition relies on. - "Add Rec LoadPath" now provides references to libraries using partially qualified names (this holds also for coqtop/coqc option -R). - SearchAbout supports negated search criteria, reference to logical objects by their notation, and more generally search of subterms. - "Declare ML Module" now allows to import .cmxs files when Coq is compiled in native code with a version of OCaml that supports native Dynlink (>= 3.11). - New command "Create HintDb name [discriminated]" to explicitely declare a new hint database and optionaly turn on a discrimination net implementation to index all the lemmas in the database. - New commands "Hint Transparent" and "Hint Opaque" to set the unfolding status of definitions used by auto. This information is taken into account by the discrimination net and the unification algorithm. - "Hint Extern" now takes an optional pattern and applies the given tactic all the time if no pattern is given. - Specific sort constraints on Record now taken into account. - "Print LoadPath" supports a path argument to filter the display. Libraries - Several parts of the libraries are now in Type, in particular FSets, SetoidList, ListSet, Sorting, Zmisc. This may induce a few incompatibilities. In case of trouble while fixing existing development, it may help to simply declare Set as an alias for Type (see file SetIsType). - New arithmetical library in theories/Numbers. It contains: * an abstract modular development of natural and integer arithmetics in Numbers/Natural/Abstract and Numbers/Integer/Abstract * an implementation of efficient computational bounded and unbounded integers that can be mapped to processor native arithmetics. See Numbers/Cyclic/Int31 for 31-bit integers and Numbers/Natural/BigN for unbounded natural numbers and Numbers/Integer/BigZ for unbounded integers. * some proofs that both older libraries Arith, ZArith and NArith and newer BigN and BigZ implement the abstract modular development. This allows in particular BigN and BigZ to already come with a large database of basic lemmas and some generic tactics (ring), This library has still an experimental status, as well as the processor-acceleration mechanism, but both its abstract and its concrete parts are already quite usable and could challenge the use of nat, N and Z in actual developments. Moreover, an extension of this framework to rational numbers is ongoing, and an efficient Q structure is already provided (see Numbers/Rational/BigQ), but this part is currently incomplete (no abstract layer and generic lemmas). - Many changes in FSets/FMaps. In practice, compatibility with earlier version should be fairly good, but some adaptations may be required. * Interfaces of unordered ("weak") and ordered sets have been factorized thanks to new features of Coq modules (in particular Include), see FSetInterface. Same for maps. Hints in these interfaces have been reworked (they are now placed in a "set" database). * To allow full subtyping between weak and ordered sets, a field "eq_dec" has been added to OrderedType. The old version of OrderedType is now called MiniOrderedType and functor MOT_to_OT allow to convert to the new version. The interfaces and implementations of sets now contain also such a "eq_dec" field. * FSetDecide, contributed by Aaron Bohannon, contains a decision procedure allowing to solve basic set-related goals (for instance, is a point in a particular set ?). See FSetProperties for examples. * Functors of properties have been improved, especially the ones about maps, that now propose some induction principles. Some properties of fold need less hypothesis. * More uniformity in implementations of sets and maps: they all use implicit arguments, and no longer export unnecessary scopes (see bug #1347) * Internal parts of the implementations based on AVL have evolved a lot. The main files FSetAVL and FMapAVL are now much more lightweight now. In particular, minor changes in some functions has allowed to fully separate the proofs of operational correctness from the proofs of well-balancing: well-balancing is critical for efficiency, but not anymore for proving that these trees implement our interfaces, hence we have moved these proofs into appendix files FSetFullAVL and FMapFullAVL. Moreover, a few functions like union and compare have been modified in order to be structural yet efficient. The appendix files also contains alternative versions of these few functions, much closer to the initial Ocaml code and written via the Function framework. - Library IntMap, subsumed by FSets/FMaps, has been removed from Coq Standard Library and moved into a user contribution Cachan/IntMap - Better computational behavior of some constants (eq_nat_dec and le_lt_dec more efficient, Z_lt_le_dec and Positive_as_OT.compare transparent, ...) (exceptional source of incompatibilities). - Boolean operators moved from module Bool to module Datatypes (may need to rename qualified references in script and force notations || and && to be at levels 50 and 40 respectively). - The constructors xI and xO of type positive now have postfix notations "~1" and "~0", allowing to write numbers in binary form easily, for instance 6 is 1~1~0 and 4*p is p~0~0 (see BinPos.v). - Improvements to NArith (Nminus, Nmin, Nmax), and to QArith (in particular a better power function). - Changes in ZArith: several additional lemmas (used in theories/Numbers), especially in Zdiv, Znumtheory, Zpower. Moreover, many results in Zdiv have been generalized: the divisor may simply be non-null instead of strictly positive (see lemmas with name ending by "_full"). An alternative file ZOdiv proposes a different behavior (the one of Ocaml) when dividing by negative numbers. - Changes in Arith: EqNat and Wf_nat now exported from Arith, some constructions on nat that were outside Arith are now in (e.g. iter_nat). - In SetoidList, eqlistA now expresses that two lists have similar elements at the same position, while the predicate previously called eqlistA is now equivlistA (this one only states that the lists contain the same elements, nothing more). - Changes in Reals: * Most statement in "sigT" (including the completeness axiom) are now in "sig" (in case of incompatibility, use proj1_sig instead of projT1, sig instead of sigT, etc). * More uniform naming scheme (identifiers in French moved to English, consistent use of 0 -- zero -- instead of O -- letter O --, etc). * Lemma on prod_f_SO is now on prod_f_R0. * Useless hypothesis of ln_exists1 dropped. * New Rlogic.v states a few logical properties about R axioms. * RIneq.v extended and made cleaner. - Slight restructuration of the Logic library regarding choice and classical logic. Addition of files providing intuitionistic axiomatizations of descriptions: Epsilon.v, Description.v and IndefiniteDescription.v. - Definition of pred and minus made compatible with the structural decreasing criterion for use in fixpoints. - Files Relations/Rstar.v and Relations/Newman.v moved out to the user contribution repository (contribution CoC_History). New lemmas about transitive closure added and some bound variables renamed (exceptional risk of incompatibilities). Notations, coercions, implicit arguments and type inference - More automation in the inference of the return clause of dependent pattern-matching problems. - Experimental allowance for omission of the clauses easily detectable as impossible in pattern-matching problems. - Improved inference of implicit arguments, now working inside record declarations. - New options "Set Maximal Implicit Insertion", "Set Reversible Pattern Implicit", "Set Strongly Strict Implicit" and "Set Printing Implicit Defensive" for controlling inference and use of implicit arguments. - New modifier in "Implicit Arguments" to force an implicit argument to be maximally inserted. - New options Global and Local to "Implicit Arguments" for section surviving or non export outside module. - Level "constr" moved from 9 to 8. - Structure/Record now printed as Record (unless option Printing All is set). - Support for parametric notations defining constants. - Insertion of coercions below product types refrains to unfold constants (possible source of incompatibility). - New support for fix/cofix in notations. Tactic Language - Second-order pattern-matching now working in Ltac "match" clauses (syntax for second-order unification variable is "@?X"). - Support for matching on let bindings in match context using syntax "H := body" or "H := body : type". - (?X ?Y) patterns now match any application instead of only unary applications (possible source of incompatibility). - Ltac accepts integer arguments (syntax is "ltac:nnn" for nnn an integer). - The general sequence tactical "expr_0 ; [ expr_1 | ... | expr_n ]" is extended so that at most one expr_i may have the form "expr .." or just "..". Also, n can be different from the number of subgoals generated by expr_0. In this case, the value of expr (or idtac in case of just "..") is applied to the intermediate subgoals to make the number of tactics equal to the number of subgoals. - A name used as the name of the parameter of a lemma (like f in "apply f_equal with (f:=t)") is now interpreted as a ltac variable if such a variable exists (this is a possible source of incompatibility and it can be fixed by renaming the variables of a ltac function into names that do not clash with the lemmas parameter names used in the tactic). - New syntax "Ltac tac ::= ..." to rebind a tactic to a new expression. - "let rec ... in ... " now supported for expressions without explicit parameters; interpretation is lazy to the contrary of "let ... in ..."; hence, the "rec" keyword can be used to turn the argument of a "let ... in ..." into a lazy one. - Patterns for hypotheses types in "match goal" are now interpreted in type_scope. - A bound variable whose name is not used elsewhere now serves as metavariable in "match" and it gets instantiated by an identifier (allow e.g. to extract the name of a statement like "exists x, P x"). - New printing of Ltac call trace for better debugging. - The C-zar (formerly know as declarative) proof language is now properly documented. Tactics - New tactics "apply -> term", "apply <- term", "apply -> term in ident", "apply <- term in ident" for applying equivalences (iff). - "apply" and "rewrite" now take open terms (terms with undefined existentials) as input. - Slight improvement of the hnf and simpl tactics when applied on expressions with explicit occurrences of match or fix. - New tactics "eapply in", "erewrite", "erewrite in". - New tactics "ediscriminate", "einjection", "esimplify_eq". - Tactics "discriminate", "injection", "simplify_eq" now support any term as argument. Clause "with" is also supported. - Unfoldable references can be given by notation's string rather than by name in unfold. - The "with" arguments are now typed using informations from the current goal: allows support for coercions and more inference of implicit arguments. - Application of "f_equal"-style lemmas works better. - Tactics elim, case, destruct and induction now support variants eelim, ecase, edestruct and einduction. - Tactics destruct and induction now support the "with" option and the "in" clause option. If the option "in" is used, an equality is added to remember the term to which the induction or case analysis applied (possible source of parsing incompatibilities when destruct or induction is part of a let-in expression in Ltac; extra parentheses are then required). - New support for "as" clause in tactics "apply in" and "eapply in". - Some new intro patterns: * intro pattern "?A" genererates a fresh name based on A. Caveat about a slight loss of compatibility: Some intro patterns don't need space between them. In particular intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it is still legal but equivalent to intros ?a ?b. * intro pattern "(A & ... & Y & Z)" synonym to "(A,....,(Y,Z)))))" for right-associative constructs like /\ or exists. - Several syntax extensions concerning "rewrite": * "rewrite A,B,C" can be used to rewrite A, then B, then C. These rewrites occur only on the first subgoal: in particular, side-conditions of the "rewrite A" are not concerned by the "rewrite B,C". * "rewrite A by tac" allows to apply tac on all side-conditions generated by the "rewrite A". * "rewrite A at n" allows to select occurrences to rewrite: rewrite only happen at the n-th exact occurrence of the first successful matching of A in the goal. * "rewrite 3 A" or "rewrite 3!A" is equivalent to "rewrite A,A,A". * "rewrite !A" means rewriting A as long as possible (and at least once). * "rewrite 3?A" means rewriting A at most three times. * "rewrite ?A" means rewriting A as long as possible (possibly never). * many of the above extensions can be combined with each other. - Introduction patterns better respect the structure of context in presence of missing or extra names in nested disjunction-conjunction patterns [possible source of rare incompatibilities]. - New syntax "rename a into b, c into d" for "rename a into b; rename c into d" - New tactics "dependent induction/destruction H [ generalizing id_1 .. id_n ]" to do induction-inversion on instantiated inductive families ? la BasicElim. - Tactics "apply" and "apply in" now able to reason modulo unfolding of constants (possible source of incompatibility in situations where apply may fail, e.g. as argument of a try or a repeat and in a ltac function); versions that do not unfold are renamed into "simple apply" and "simple apply in" (usable for compatibility or for automation). - Tactics "apply" and "apply in" now able to traverse conjunctions and to select the first matching lemma among the components of the conjunction; tactic "apply" also able to apply lemmas of conclusion an empty type. - Tactic "apply" now supports application of several lemmas in a row. - Tactics "set" and "pose" can set functions using notation "(f x1..xn := c)". - New tactic "instantiate" (without argument). - Tactic firstorder "with" and "using" options have their meaning swapped for consistency with auto/eauto (source of incompatibility). - Tactic "generalize" now supports "at" options to specify occurrences and "as" options to name the quantified hypotheses. - New tactic "specialize H with a" or "specialize (H a)" allows to transform in-place a universally-quantified hypothesis (H : forall x, T x) into its instantiated form (H : T a). Nota: "specialize" was in fact there in earlier versions of Coq, but was undocumented, and had a slightly different behavior. - New tactic "contradict H" can be used to solve any kind of goal as long as the user can provide afterwards a proof of the negation of the hypothesis H. If H is already a negation, say ~T, then a proof of T is asked. If the current goal is a negation, say ~U, then U is saved in H afterwards, hence this new tactic "contradict" extends earlier tactic "swap", which is now obsolete. - Tactics f_equal is now done in ML instead of Ltac: it now works on any equality of functions, regardless of the arity of the function. - New options "before id", "at top", "at bottom" for tactics "move"/"intro". - Some more debug of reflexive omega (romega), and internal clarifications. Moreover, romega now has a variant "romega with *" that can be also used on non-Z goals (nat, N, positive) via a call to a translation tactic named zify (its purpose is to Z-ify your goal...). This zify may also be used independantly of romega. - Tactic "remember" now supports an "in" clause to remember only selected occurrences of a term. - Tactic "pose proof" supports name overwriting in case of specialization of an hypothesis. - Semi-decision tactic "jp" for first-order intuitionistic logic moved to user contributions (subsumed by "firstorder"). Program - Moved useful tactics in theories/Program and documented them. - Add Program.Basics which contains standard definitions for functional programming (id, apply, flip...) - More robust obligation handling, dependent pattern-matching and well-founded definitions. - Program CoFixpoint is accepted, Program Fixpoint uses the new way to infer which argument decreases structurally. - Program Lemma, Axiom etc... now permit to have obligations in the statement iff they can be automatically solved by the default tactic. - Renamed "Obligations Tactic" command to "Obligation Tactic". - New command "Preterm [ of id ]" to see the actual term fed to Coq for debugging purposes. - New option "Transparent Obligations" to control the declaration of obligations as transparent or opaque. All obligations are now transparent by default, otherwise the system declares them opaque if possible. - Changed the notations "left" and "right" to "in_left" and "in_right" to hide the proofs in standard disjunctions, to avoid breaking existing scripts when importing Program. Also, put them in program_scope. Type Classes - New "Class", "Instance" and "Program Instance" commands to define classes and instances documented in the reference manual. - New binding construct "`{Class_1 param_1 .. param_n, Class_2 ...}" for binding type classes, usable everywhere. - New command " Print Classes " and " Print Instances some_class " to print tables for typeclasses. - New default eauto hint database "typeclass_instances" used by the default typeclass instance search tactic. - New theories directory "theories/Classes" for standard typeclasses declarations. Module Classes.RelationClasses is a typeclass port of Relation_Definitions plus a generic development of algebra on n-ary heterogeneous predicates. Setoid rewriting - Complete (and still experimental) rewrite of the tactic based on typeclasses. The old interface and semantics are almost entirely respected, except: - Import Setoid is now mandatory to be able to call setoid_replace and declare morphisms. - "-->", "++>" and "==>" are now right associative notations declared at level 55 in scope signature_scope. Their introduction may break existing scripts that defined them as notations with different levels. - One can use [Typeclasses Opaque/Transparent [cst]] to indicate that [cst] should not be unfolded during unification for morphism resolution, by default all constants are transparent. - The [setoid_rewrite]'s semantics change when rewriting with a lemma: it can rewrite two different instantiations of the lemma at once. Use [setoid_rewrite H at 1] for (almost) the usual semantics. [setoid_rewrite] will also try to rewrite under binders now, and can succeed on different terms than before. In particular, it will unify under let-bound variables. When called through [rewrite], the semantics are unchanged though. - [Add Morphism term : id] has different semantics when used with parametric morphism: it will try to find a relation on the parameters too. The behavior has also changed with respect to default relations: the most recently declared Setoid/Relation will be used, the documentation explains how to customize this behavior. - Parametric Relation and Morphism are declared differently, using the new [Add Parametric] commands, documented in the manual. - Setoid_Theory is now an alias to Equivalence, scripts building objects of type Setoid_Theory need to unfold (or [red]) the definitions of Reflexive, Symmetric and Transitive in order to get the same goals as before. Scripts which introduced variables explicitely will not break. - The order of subgoals when doing [setoid_rewrite] with side-conditions is now always the same: first the new goal, then the conditions. - New standard library modules Classes.Morphisms declares standard morphisms on refl/sym/trans relations. Classes.Morphisms_Prop declares morphisms on propositional connectives and Classes.Morphisms_Relations on generalized predicate connectives. Classes.Equivalence declares notations and tactics related to equivalences and Classes.SetoidTactics defines the setoid_replace tactics and some support for the "Add *" interface, notably the tactic applied automatically before each "Add Morphism" proof. - User-defined subrelations are supported, as well as higher-order morphisms and rewriting under binders. The tactic is also extensible entirely in Ltac. The documentation has been updated to cover these features. - [setoid_rewrite] and [rewrite] now support the [at] modifier to select occurrences to rewrite, and both use the [setoid_rewrite] code, even when rewriting with leibniz equality if occurrences are specified. Extraction - Improved behavior of the Caml extraction of modules: name clashes should not happen anymore. - The command Extract Inductive has now a syntax for infix notations. This allows in particular to map Coq lists and pairs onto Caml ones: Extract Inductive list => list [ "[]" "(::)" ]. Extract Inductive prod => "(*)" [ "(,)" ]. - In pattern matchings, a default pattern "| _ -> ..." is now used whenever possible if several branches are identical. For instance, functions corresponding to decidability of equalities are now linear instead of quadratic. - A new instruction Extraction Blacklist id1 .. idn allows to prevent filename conflits with existing code, for instance when extracting module List to Ocaml. CoqIDE - CoqIDE font defaults to monospace so as indentation to be meaningful. - CoqIDE supports nested goals and any other kind of declaration in the middle of a proof. - Undoing non-tactic commands in CoqIDE works faster. - New CoqIDE menu for activating display of various implicit informations. - Added the possibility to choose the location of tabs in coqide: (in Edit->Preferences->Misc) - New Open and Save As dialogs in CoqIDE which filter *.v files. Tools - New stand-alone .vo files verifier "coqchk". - Extended -I coqtop/coqc option to specify a logical dir: "-I dir -as coqdir". - New coqtop/coqc option -exclude-dir to exclude subdirs for option -R. - The binary "parser" has been renamed to "coq-parser". coqdoc - Improved coqdoc and dump of globalization information to give more meta-information on identifiers. All categories of Coq definitions are supported, which makes typesetting trivial in the generated documentation. - A "--interpolate" option permits to use typesetting information from the typechecked part of the file to typeset identifiers appearing in Coq escapings inside the documentation. - Better handling of utf8 ("--utf8" option) and respect of spaces in the source. - Support for hyperlinking and indexing developments in the TeX output. - New option "color" of the coqdoc style file to render identifiers using colors. - Additional macros in the TeX ouput allowing to customize indentation and size of empty lines. New environment "coqdoccode" for Coq code. Miscellaneous - Coq installation provides enough files so that Ocaml's extensions need not the Coq sources to be compiled (this assumes O'Caml 3.10 and Camlp5). - New commands "Set Whelp Server" and "Set Whelp Getter" to customize the Whelp search tool. - Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into "Test Printing Let for ref" and "Test Printing If for ref". - An overhauled build system (new Makefiles); see dev/doc/build-system.txt. - Add -browser option to configure script. - Build a shared library for the C part of Coq, and use it by default on non-(Windows or MacOS) systems. Bytecode executables are now pure. The behaviour is configurable with -coqrunbyteflags, -coqtoolsbyteflags and -custom configure options. - Complexity tests can be skipped by setting the environment variable COQTEST_SKIPCOMPLEXITY.
Diffstat (limited to 'lang/coq')
-rw-r--r--lang/coq/Makefile13
-rw-r--r--lang/coq/PLIST505
-rw-r--r--lang/coq/PLIST.opt5
-rw-r--r--lang/coq/distinfo13
-rw-r--r--lang/coq/patches/patch-aa173
-rw-r--r--lang/coq/patches/patch-ab17
-rw-r--r--lang/coq/patches/patch-ac12
7 files changed, 498 insertions, 240 deletions
diff --git a/lang/coq/Makefile b/lang/coq/Makefile
index 2412f8e2110..14414ea6364 100644
--- a/lang/coq/Makefile
+++ b/lang/coq/Makefile
@@ -1,10 +1,9 @@
-# $NetBSD: Makefile,v 1.22 2009/08/26 19:57:54 sno Exp $
+# $NetBSD: Makefile,v 1.23 2009/09/05 20:44:57 tonio Exp $
#
-DISTNAME= coq-8.1pl3
-PKGREVISION= 2
+DISTNAME= coq-8.2pl1
CATEGORIES= lang math
-MASTER_SITES= ftp://ftp.inria.fr/INRIA/coq/V8.1pl3/
+MASTER_SITES= http://coq.inria.fr/distrib/V8.2pl1/files/
MAINTAINER= richards+netbsd@CS.Princeton.EDU
HOMEPAGE= http://coq.inria.fr/
@@ -17,7 +16,7 @@ CONFIGURE_ARGS+= -emacslib ${PREFIX}/share/emacs/site-lisp
CONFIGURE_ARGS+= -reals all
BUILD_TARGET= world
-BUILDLINK_API_DEPENDS.ocaml+= ocaml>=3.09
+BUILDLINK_API_DEPENDS.ocaml+= ocaml>=3.10
.include "../../mk/bsd.prefs.mk"
@@ -34,6 +33,10 @@ _STRIPFLAG_CC=
_STRIPFLAG_INSTALL=
.endif
+REPLACE_SH= configure install.sh
+CONFIGURE_ENV+= SHELL=${SH:Q}
+MAKE_ENV+= SHELL=${SH:Q}
+
PLIST_VARS= coqide
PKG_OPTIONS_VAR= PKG_OPTIONS.coq
PKG_SUPPORTED_OPTIONS= coqide
diff --git a/lang/coq/PLIST b/lang/coq/PLIST
index ceca5865564..7f1dc99f3d8 100644
--- a/lang/coq/PLIST
+++ b/lang/coq/PLIST
@@ -1,8 +1,10 @@
-@comment $NetBSD: PLIST,v 1.9 2009/06/14 20:34:13 joerg Exp $
+@comment $NetBSD: PLIST,v 1.10 2009/09/05 20:44:57 tonio Exp $
bin/coq-interface
+bin/coq-parser
bin/coq-tex
bin/coq_makefile
bin/coqc
+bin/coqchk
bin/coqdep
bin/coqdoc
${PLIST.coqide}bin/coqide
@@ -12,17 +14,89 @@ bin/coqtop
bin/coqtop.byte
bin/coqwc
bin/gallina
-bin/parser
+lib/coq/config/coq_config.cmi
+lib/coq/config/coq_config.cmo
+lib/coq/config/coq_config.cmx
+lib/coq/config/coq_config.o
+lib/coq/contrib/cc/ccalgo.cmi
+lib/coq/contrib/cc/ccproof.cmi
+lib/coq/contrib/cc/cctac.cmi
+lib/coq/contrib/cc/g_congruence.cmi
+lib/coq/contrib/contrib.a
+lib/coq/contrib/contrib.cma
+lib/coq/contrib/contrib.cmxa
+lib/coq/contrib/dp/Dp.vo
+lib/coq/contrib/dp/dp.cmi
+lib/coq/contrib/dp/dp_gappa.cmi
+lib/coq/contrib/dp/dp_why.cmi
+lib/coq/contrib/dp/dp_zenon.cmi
+lib/coq/contrib/dp/g_dp.cmi
+lib/coq/contrib/extraction/common.cmi
+lib/coq/contrib/extraction/extract_env.cmi
+lib/coq/contrib/extraction/extraction.cmi
+lib/coq/contrib/extraction/g_extraction.cmi
+lib/coq/contrib/extraction/haskell.cmi
+lib/coq/contrib/extraction/mlutil.cmi
+lib/coq/contrib/extraction/modutil.cmi
+lib/coq/contrib/extraction/ocaml.cmi
+lib/coq/contrib/extraction/scheme.cmi
+lib/coq/contrib/extraction/table.cmi
lib/coq/contrib/field/LegacyField.vo
lib/coq/contrib/field/LegacyField_Compl.vo
lib/coq/contrib/field/LegacyField_Tactic.vo
lib/coq/contrib/field/LegacyField_Theory.vo
+lib/coq/contrib/field/field.cmi
+lib/coq/contrib/firstorder/formula.cmi
+lib/coq/contrib/firstorder/g_ground.cmi
+lib/coq/contrib/firstorder/ground.cmi
+lib/coq/contrib/firstorder/instances.cmi
+lib/coq/contrib/firstorder/rules.cmi
+lib/coq/contrib/firstorder/sequent.cmi
+lib/coq/contrib/firstorder/unify.cmi
lib/coq/contrib/fourier/Fourier.vo
lib/coq/contrib/fourier/Fourier_util.vo
+lib/coq/contrib/fourier/fourier.cmi
+lib/coq/contrib/fourier/fourierR.cmi
+lib/coq/contrib/fourier/g_fourier.cmi
+lib/coq/contrib/funind/Recdef.vo
+lib/coq/contrib/funind/functional_principles_proofs.cmi
+lib/coq/contrib/funind/functional_principles_types.cmi
+lib/coq/contrib/funind/g_indfun.cmi
+lib/coq/contrib/funind/indfun.cmi
+lib/coq/contrib/funind/indfun_common.cmi
+lib/coq/contrib/funind/invfun.cmi
+lib/coq/contrib/funind/merge.cmi
+lib/coq/contrib/funind/rawterm_to_relation.cmi
+lib/coq/contrib/funind/rawtermops.cmi
+lib/coq/contrib/funind/recdef.cmi
lib/coq/contrib/interface/vernacrc
+lib/coq/contrib/micromega/CheckerMaker.vo
+lib/coq/contrib/micromega/Env.vo
+lib/coq/contrib/micromega/EnvRing.vo
+lib/coq/contrib/micromega/OrderedRing.vo
+lib/coq/contrib/micromega/Psatz.vo
+lib/coq/contrib/micromega/QMicromega.vo
+lib/coq/contrib/micromega/RMicromega.vo
+lib/coq/contrib/micromega/Refl.vo
+lib/coq/contrib/micromega/RingMicromega.vo
+lib/coq/contrib/micromega/Tauto.vo
+lib/coq/contrib/micromega/VarMap.vo
+lib/coq/contrib/micromega/ZCoeff.vo
+lib/coq/contrib/micromega/ZMicromega.vo
+lib/coq/contrib/micromega/certificate.cmi
+lib/coq/contrib/micromega/coq_micromega.cmi
+lib/coq/contrib/micromega/csdpcert
+lib/coq/contrib/micromega/g_micromega.cmi
+lib/coq/contrib/micromega/mfourier.cmi
+lib/coq/contrib/micromega/micromega.cmi
+lib/coq/contrib/micromega/mutils.cmi
+lib/coq/contrib/micromega/vector.cmi
lib/coq/contrib/omega/Omega.vo
lib/coq/contrib/omega/OmegaLemmas.vo
-lib/coq/contrib/recdef/Recdef.vo
+lib/coq/contrib/omega/PreOmega.vo
+lib/coq/contrib/omega/coq_omega.cmi
+lib/coq/contrib/omega/g_omega.cmi
+lib/coq/contrib/omega/omega.cmi
lib/coq/contrib/ring/LegacyArithRing.vo
lib/coq/contrib/ring/LegacyNArithRing.vo
lib/coq/contrib/ring/LegacyRing.vo
@@ -34,10 +108,20 @@ lib/coq/contrib/ring/Ring_normalize.vo
lib/coq/contrib/ring/Setoid_ring.vo
lib/coq/contrib/ring/Setoid_ring_normalize.vo
lib/coq/contrib/ring/Setoid_ring_theory.vo
+lib/coq/contrib/ring/g_quote.cmi
+lib/coq/contrib/ring/g_ring.cmi
+lib/coq/contrib/ring/quote.cmi
+lib/coq/contrib/ring/ring.cmi
lib/coq/contrib/romega/ROmega.vo
lib/coq/contrib/romega/ReflOmegaCore.vo
+lib/coq/contrib/romega/const_omega.cmi
+lib/coq/contrib/romega/g_romega.cmi
+lib/coq/contrib/romega/refl_omega.cmi
lib/coq/contrib/rtauto/Bintree.vo
lib/coq/contrib/rtauto/Rtauto.vo
+lib/coq/contrib/rtauto/g_rtauto.cmi
+lib/coq/contrib/rtauto/proof_search.cmi
+lib/coq/contrib/rtauto/refl_tauto.cmi
lib/coq/contrib/setoid_ring/ArithRing.vo
lib/coq/contrib/setoid_ring/BinList.vo
lib/coq/contrib/setoid_ring/Field.vo
@@ -53,42 +137,244 @@ lib/coq/contrib/setoid_ring/Ring_polynom.vo
lib/coq/contrib/setoid_ring/Ring_tac.vo
lib/coq/contrib/setoid_ring/Ring_theory.vo
lib/coq/contrib/setoid_ring/ZArithRing.vo
-lib/coq/contrib/subtac/FixSub.vo
-lib/coq/contrib/subtac/FunctionalExtensionality.vo
-lib/coq/contrib/subtac/Heq.vo
-lib/coq/contrib/subtac/Subtac.vo
-lib/coq/contrib/subtac/SubtacTactics.vo
-lib/coq/contrib/subtac/Utils.vo
+lib/coq/contrib/setoid_ring/newring.cmi
+lib/coq/contrib/subtac/equations.cmi
+lib/coq/contrib/subtac/eterm.cmi
+lib/coq/contrib/subtac/g_eterm.cmi
+lib/coq/contrib/subtac/g_subtac.cmi
+lib/coq/contrib/subtac/subtac.cmi
+lib/coq/contrib/subtac/subtac_cases.cmi
+lib/coq/contrib/subtac/subtac_classes.cmi
+lib/coq/contrib/subtac/subtac_coercion.cmi
+lib/coq/contrib/subtac/subtac_command.cmi
+lib/coq/contrib/subtac/subtac_errors.cmi
+lib/coq/contrib/subtac/subtac_obligations.cmi
+lib/coq/contrib/subtac/subtac_pretyping.cmi
+lib/coq/contrib/subtac/subtac_pretyping_F.cmi
+lib/coq/contrib/subtac/subtac_utils.cmi
+lib/coq/contrib/xml/acic.cmi
+lib/coq/contrib/xml/acic2Xml.cmi
+lib/coq/contrib/xml/cic2Xml.cmi
+lib/coq/contrib/xml/cic2acic.cmi
+lib/coq/contrib/xml/doubleTypeInference.cmi
+lib/coq/contrib/xml/dumptree.cmi
+lib/coq/contrib/xml/proof2aproof.cmi
+lib/coq/contrib/xml/proofTree2Xml.cmi
+lib/coq/contrib/xml/unshare.cmi
+lib/coq/contrib/xml/xml.cmi
+lib/coq/contrib/xml/xmlcommand.cmi
+lib/coq/contrib/xml/xmlentries.cmi
+lib/coq/dllcoqrun.so
lib/coq/ide/.coqide-gtk2rc
lib/coq/ide/FAQ
lib/coq/ide/coq.png
-lib/coq/ide/utf8.v
-lib/coq/ide/utf8.vo
-lib/coq/states/contrib.cma
-lib/coq/states/contrib.cmxa
-lib/coq/states/highparsing.cma
-lib/coq/states/highparsing.cmxa
-lib/coq/states/hightactics.cma
-lib/coq/states/hightactics.cmxa
+lib/coq/interp/constrextern.cmi
+lib/coq/interp/constrintern.cmi
+lib/coq/interp/coqlib.cmi
+lib/coq/interp/dumpglob.cmi
+lib/coq/interp/genarg.cmi
+lib/coq/interp/implicit_quantifiers.cmi
+lib/coq/interp/interp.a
+lib/coq/interp/interp.cma
+lib/coq/interp/interp.cmxa
+lib/coq/interp/modintern.cmi
+lib/coq/interp/notation.cmi
+lib/coq/interp/ppextend.cmi
+lib/coq/interp/reserve.cmi
+lib/coq/interp/syntax_def.cmi
+lib/coq/interp/topconstr.cmi
+lib/coq/kernel/cbytecodes.cmi
+lib/coq/kernel/cbytegen.cmi
+lib/coq/kernel/cemitcodes.cmi
+lib/coq/kernel/closure.cmi
+lib/coq/kernel/conv_oracle.cmi
+lib/coq/kernel/cooking.cmi
+lib/coq/kernel/copcodes.cmi
+lib/coq/kernel/csymtable.cmi
+lib/coq/kernel/declarations.cmi
+lib/coq/kernel/entries.cmi
+lib/coq/kernel/environ.cmi
+lib/coq/kernel/esubst.cmi
+lib/coq/kernel/indtypes.cmi
+lib/coq/kernel/inductive.cmi
+lib/coq/kernel/kernel.a
+lib/coq/kernel/kernel.cma
+lib/coq/kernel/kernel.cmxa
+lib/coq/kernel/mod_subst.cmi
+lib/coq/kernel/mod_typing.cmi
+lib/coq/kernel/modops.cmi
+lib/coq/kernel/names.cmi
+lib/coq/kernel/pre_env.cmi
+lib/coq/kernel/reduction.cmi
+lib/coq/kernel/retroknowledge.cmi
+lib/coq/kernel/safe_typing.cmi
+lib/coq/kernel/sign.cmi
+lib/coq/kernel/subtyping.cmi
+lib/coq/kernel/term.cmi
+lib/coq/kernel/term_typing.cmi
+lib/coq/kernel/type_errors.cmi
+lib/coq/kernel/typeops.cmi
+lib/coq/kernel/univ.cmi
+lib/coq/kernel/vconv.cmi
+lib/coq/kernel/vm.cmi
+lib/coq/lib/bigint.cmi
+lib/coq/lib/bstack.cmi
+lib/coq/lib/compat.cmi
+lib/coq/lib/dyn.cmi
+lib/coq/lib/edit.cmi
+lib/coq/lib/envars.cmi
+lib/coq/lib/explore.cmi
+lib/coq/lib/flags.cmi
+lib/coq/lib/gmap.cmi
+lib/coq/lib/gmapl.cmi
+lib/coq/lib/gset.cmi
+lib/coq/lib/hashcons.cmi
+lib/coq/lib/heap.cmi
+lib/coq/lib/lib.a
+lib/coq/lib/lib.cma
+lib/coq/lib/lib.cmxa
+lib/coq/lib/option.cmi
+lib/coq/lib/pp.cmi
+lib/coq/lib/pp_control.cmi
+lib/coq/lib/predicate.cmi
+lib/coq/lib/profile.cmi
+lib/coq/lib/rtree.cmi
+lib/coq/lib/system.cmi
+lib/coq/lib/tlm.cmi
+lib/coq/lib/util.cmi
+lib/coq/libcoqrun.a
+lib/coq/library/decl_kinds.cmi
+lib/coq/library/declare.cmi
+lib/coq/library/declaremods.cmi
+lib/coq/library/decls.cmi
+lib/coq/library/dischargedhypsmap.cmi
+lib/coq/library/global.cmi
+lib/coq/library/goptions.cmi
+lib/coq/library/heads.cmi
+lib/coq/library/impargs.cmi
+lib/coq/library/lib.cmi
+lib/coq/library/libnames.cmi
+lib/coq/library/libobject.cmi
+lib/coq/library/library.a
+lib/coq/library/library.cma
+lib/coq/library/library.cmi
+lib/coq/library/library.cmxa
+lib/coq/library/nameops.cmi
+lib/coq/library/nametab.cmi
+lib/coq/library/states.cmi
+lib/coq/library/summary.cmi
+lib/coq/parsing/egrammar.cmi
+lib/coq/parsing/extend.cmi
+lib/coq/parsing/g_ascii_syntax.cmi
+lib/coq/parsing/g_constr.cmi
+lib/coq/parsing/g_decl_mode.cmi
+lib/coq/parsing/g_intsyntax.cmi
+lib/coq/parsing/g_ltac.cmi
+lib/coq/parsing/g_natsyntax.cmi
+lib/coq/parsing/g_prim.cmi
+lib/coq/parsing/g_proofs.cmi
+lib/coq/parsing/g_rsyntax.cmi
+lib/coq/parsing/g_string_syntax.cmi
+lib/coq/parsing/g_tactic.cmi
+lib/coq/parsing/g_vernac.cmi
+lib/coq/parsing/g_xml.cmi
+lib/coq/parsing/g_zsyntax.cmi
+lib/coq/parsing/grammar.cma
+lib/coq/parsing/highparsing.a
+lib/coq/parsing/highparsing.cma
+lib/coq/parsing/highparsing.cmxa
+lib/coq/parsing/lexer.cmi
+lib/coq/parsing/parsing.a
+lib/coq/parsing/parsing.cma
+lib/coq/parsing/parsing.cmxa
+lib/coq/parsing/pcoq.cmi
+lib/coq/parsing/ppconstr.cmi
+lib/coq/parsing/ppdecl_proof.cmi
+lib/coq/parsing/pptactic.cmi
+lib/coq/parsing/ppvernac.cmi
+lib/coq/parsing/prettyp.cmi
+lib/coq/parsing/printer.cmi
+lib/coq/parsing/printmod.cmi
+lib/coq/parsing/search.cmi
+lib/coq/parsing/tactic_printer.cmi
+lib/coq/pretyping/cases.cmi
+lib/coq/pretyping/cbv.cmi
+lib/coq/pretyping/classops.cmi
+lib/coq/pretyping/clenv.cmi
+lib/coq/pretyping/coercion.cmi
+lib/coq/pretyping/detyping.cmi
+lib/coq/pretyping/evarconv.cmi
+lib/coq/pretyping/evarutil.cmi
+lib/coq/pretyping/evd.cmi
+lib/coq/pretyping/indrec.cmi
+lib/coq/pretyping/inductiveops.cmi
+lib/coq/pretyping/matching.cmi
+lib/coq/pretyping/pattern.cmi
+lib/coq/pretyping/pretype_errors.cmi
+lib/coq/pretyping/pretyping.a
+lib/coq/pretyping/pretyping.cma
+lib/coq/pretyping/pretyping.cmi
+lib/coq/pretyping/pretyping.cmxa
+lib/coq/pretyping/rawterm.cmi
+lib/coq/pretyping/recordops.cmi
+lib/coq/pretyping/reductionops.cmi
+lib/coq/pretyping/retyping.cmi
+lib/coq/pretyping/tacred.cmi
+lib/coq/pretyping/termops.cmi
+lib/coq/pretyping/typeclasses.cmi
+lib/coq/pretyping/typeclasses_errors.cmi
+lib/coq/pretyping/typing.cmi
+lib/coq/pretyping/unification.cmi
+lib/coq/pretyping/vnorm.cmi
+lib/coq/proofs/clenvtac.cmi
+lib/coq/proofs/decl_mode.cmi
+lib/coq/proofs/evar_refiner.cmi
+lib/coq/proofs/logic.cmi
+lib/coq/proofs/pfedit.cmi
+lib/coq/proofs/proof_trees.cmi
+lib/coq/proofs/proof_type.cmi
+lib/coq/proofs/proofs.a
+lib/coq/proofs/proofs.cma
+lib/coq/proofs/proofs.cmxa
+lib/coq/proofs/redexpr.cmi
+lib/coq/proofs/refiner.cmi
+lib/coq/proofs/tacexpr.cmi
+lib/coq/proofs/tacmach.cmi
+lib/coq/proofs/tactic_debug.cmi
lib/coq/states/initial.coq
-lib/coq/states/interp.cma
-lib/coq/states/interp.cmxa
-lib/coq/states/kernel.cma
-lib/coq/states/kernel.cmxa
-lib/coq/states/lib.cma
-lib/coq/states/lib.cmxa
-lib/coq/states/library.cma
-lib/coq/states/library.cmxa
-lib/coq/states/parsing.cma
-lib/coq/states/parsing.cmxa
-lib/coq/states/pretyping.cma
-lib/coq/states/pretyping.cmxa
-lib/coq/states/proofs.cma
-lib/coq/states/proofs.cmxa
-lib/coq/states/tactics.cma
-lib/coq/states/tactics.cmxa
-lib/coq/states/toplevel.cma
-lib/coq/states/toplevel.cmxa
+lib/coq/tactics/auto.cmi
+lib/coq/tactics/autorewrite.cmi
+lib/coq/tactics/btermdn.cmi
+lib/coq/tactics/class_tactics.cmi
+lib/coq/tactics/contradiction.cmi
+lib/coq/tactics/decl_interp.cmi
+lib/coq/tactics/decl_proof_instr.cmi
+lib/coq/tactics/dhyp.cmi
+lib/coq/tactics/dn.cmi
+lib/coq/tactics/eauto.cmi
+lib/coq/tactics/elim.cmi
+lib/coq/tactics/eqdecide.cmi
+lib/coq/tactics/equality.cmi
+lib/coq/tactics/evar_tactics.cmi
+lib/coq/tactics/extraargs.cmi
+lib/coq/tactics/extratactics.cmi
+lib/coq/tactics/hiddentac.cmi
+lib/coq/tactics/hightactics.a
+lib/coq/tactics/hightactics.cma
+lib/coq/tactics/hightactics.cmxa
+lib/coq/tactics/hipattern.cmi
+lib/coq/tactics/inv.cmi
+lib/coq/tactics/leminv.cmi
+lib/coq/tactics/nbtermdn.cmi
+lib/coq/tactics/refine.cmi
+lib/coq/tactics/tacinterp.cmi
+lib/coq/tactics/tacticals.cmi
+lib/coq/tactics/tactics.a
+lib/coq/tactics/tactics.cma
+lib/coq/tactics/tactics.cmi
+lib/coq/tactics/tactics.cmxa
+lib/coq/tactics/tauto.cmi
+lib/coq/tactics/termdn.cmi
lib/coq/theories/Arith/Arith.vo
lib/coq/theories/Arith/Arith_base.vo
lib/coq/theories/Arith/Between.vo
@@ -117,30 +403,37 @@ lib/coq/theories/Bool/DecBool.vo
lib/coq/theories/Bool/IfProp.vo
lib/coq/theories/Bool/Sumbool.vo
lib/coq/theories/Bool/Zerob.vo
+lib/coq/theories/Classes/EquivDec.vo
+lib/coq/theories/Classes/Equivalence.vo
+lib/coq/theories/Classes/Functions.vo
+lib/coq/theories/Classes/Init.vo
+lib/coq/theories/Classes/Morphisms.vo
+lib/coq/theories/Classes/Morphisms_Prop.vo
+lib/coq/theories/Classes/Morphisms_Relations.vo
+lib/coq/theories/Classes/RelationClasses.vo
+lib/coq/theories/Classes/SetoidAxioms.vo
+lib/coq/theories/Classes/SetoidClass.vo
+lib/coq/theories/Classes/SetoidDec.vo
+lib/coq/theories/Classes/SetoidTactics.vo
lib/coq/theories/FSets/FMapAVL.vo
lib/coq/theories/FSets/FMapFacts.vo
-lib/coq/theories/FSets/FMapIntMap.vo
+lib/coq/theories/FSets/FMapFullAVL.vo
lib/coq/theories/FSets/FMapInterface.vo
lib/coq/theories/FSets/FMapList.vo
lib/coq/theories/FSets/FMapPositive.vo
-lib/coq/theories/FSets/FMapWeak.vo
-lib/coq/theories/FSets/FMapWeakFacts.vo
-lib/coq/theories/FSets/FMapWeakInterface.vo
lib/coq/theories/FSets/FMapWeakList.vo
lib/coq/theories/FSets/FMaps.vo
lib/coq/theories/FSets/FSetAVL.vo
lib/coq/theories/FSets/FSetBridge.vo
+lib/coq/theories/FSets/FSetDecide.vo
lib/coq/theories/FSets/FSetEqProperties.vo
lib/coq/theories/FSets/FSetFacts.vo
+lib/coq/theories/FSets/FSetFullAVL.vo
lib/coq/theories/FSets/FSetInterface.vo
lib/coq/theories/FSets/FSetList.vo
lib/coq/theories/FSets/FSetProperties.vo
lib/coq/theories/FSets/FSetToFiniteSet.vo
-lib/coq/theories/FSets/FSetWeak.vo
-lib/coq/theories/FSets/FSetWeakFacts.vo
-lib/coq/theories/FSets/FSetWeakInterface.vo
lib/coq/theories/FSets/FSetWeakList.vo
-lib/coq/theories/FSets/FSetWeakProperties.vo
lib/coq/theories/FSets/FSets.vo
lib/coq/theories/FSets/OrderedType.vo
lib/coq/theories/FSets/OrderedTypeAlt.vo
@@ -154,24 +447,12 @@ lib/coq/theories/Init/Prelude.vo
lib/coq/theories/Init/Specif.vo
lib/coq/theories/Init/Tactics.vo
lib/coq/theories/Init/Wf.vo
-lib/coq/theories/IntMap/Adalloc.vo
-lib/coq/theories/IntMap/Allmaps.vo
-lib/coq/theories/IntMap/Fset.vo
-lib/coq/theories/IntMap/Lsort.vo
-lib/coq/theories/IntMap/Map.vo
-lib/coq/theories/IntMap/Mapaxioms.vo
-lib/coq/theories/IntMap/Mapc.vo
-lib/coq/theories/IntMap/Mapcanon.vo
-lib/coq/theories/IntMap/Mapcard.vo
-lib/coq/theories/IntMap/Mapfold.vo
-lib/coq/theories/IntMap/Mapiter.vo
-lib/coq/theories/IntMap/Maplists.vo
-lib/coq/theories/IntMap/Mapsubset.vo
lib/coq/theories/Lists/List.vo
lib/coq/theories/Lists/ListSet.vo
lib/coq/theories/Lists/ListTactics.vo
lib/coq/theories/Lists/MonoList.vo
lib/coq/theories/Lists/SetoidList.vo
+lib/coq/theories/Lists/StreamMemo.vo
lib/coq/theories/Lists/Streams.vo
lib/coq/theories/Lists/TheoryList.vo
lib/coq/theories/Logic/Berardi.vo
@@ -190,15 +471,20 @@ lib/coq/theories/Logic/ConstructiveEpsilon.vo
lib/coq/theories/Logic/Decidable.vo
lib/coq/theories/Logic/DecidableType.vo
lib/coq/theories/Logic/DecidableTypeEx.vo
+lib/coq/theories/Logic/Description.vo
lib/coq/theories/Logic/Diaconescu.vo
+lib/coq/theories/Logic/Epsilon.vo
lib/coq/theories/Logic/Eqdep.vo
lib/coq/theories/Logic/EqdepFacts.vo
lib/coq/theories/Logic/Eqdep_dec.vo
+lib/coq/theories/Logic/FunctionalExtensionality.vo
lib/coq/theories/Logic/Hurkens.vo
+lib/coq/theories/Logic/IndefiniteDescription.vo
lib/coq/theories/Logic/JMeq.vo
lib/coq/theories/Logic/ProofIrrelevance.vo
lib/coq/theories/Logic/ProofIrrelevanceFacts.vo
lib/coq/theories/Logic/RelationalChoice.vo
+lib/coq/theories/Logic/SetIsType.vo
lib/coq/theories/NArith/BinNat.vo
lib/coq/theories/NArith/BinPos.vo
lib/coq/theories/NArith/NArith.vo
@@ -207,12 +493,83 @@ lib/coq/theories/NArith/Ndigits.vo
lib/coq/theories/NArith/Ndist.vo
lib/coq/theories/NArith/Nnat.vo
lib/coq/theories/NArith/Pnat.vo
+lib/coq/theories/Numbers/BigNumPrelude.vo
+lib/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.vo
+lib/coq/theories/Numbers/Cyclic/Abstract/NZCyclic.vo
+lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.vo
+lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.vo
+lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.vo
+lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.vo
+lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.vo
+lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.vo
+lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.vo
+lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.vo
+lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.vo
+lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.vo
+lib/coq/theories/Numbers/Cyclic/Int31/Cyclic31.vo
+lib/coq/theories/Numbers/Cyclic/Int31/Int31.vo
+lib/coq/theories/Numbers/Cyclic/ZModulo/ZModulo.vo
+lib/coq/theories/Numbers/Integer/Abstract/ZAdd.vo
+lib/coq/theories/Numbers/Integer/Abstract/ZAddOrder.vo
+lib/coq/theories/Numbers/Integer/Abstract/ZAxioms.vo
+lib/coq/theories/Numbers/Integer/Abstract/ZBase.vo
+lib/coq/theories/Numbers/Integer/Abstract/ZLt.vo
+lib/coq/theories/Numbers/Integer/Abstract/ZMul.vo
+lib/coq/theories/Numbers/Integer/Abstract/ZMulOrder.vo
+lib/coq/theories/Numbers/Integer/BigZ/BigZ.vo
+lib/coq/theories/Numbers/Integer/BigZ/ZMake.vo
+lib/coq/theories/Numbers/Integer/Binary/ZBinary.vo
+lib/coq/theories/Numbers/Integer/NatPairs/ZNatPairs.vo
+lib/coq/theories/Numbers/Integer/SpecViaZ/ZSig.vo
+lib/coq/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.vo
+lib/coq/theories/Numbers/NaryFunctions.vo
+lib/coq/theories/Numbers/NatInt/NZAdd.vo
+lib/coq/theories/Numbers/NatInt/NZAddOrder.vo
+lib/coq/theories/Numbers/NatInt/NZAxioms.vo
+lib/coq/theories/Numbers/NatInt/NZBase.vo
+lib/coq/theories/Numbers/NatInt/NZMul.vo
+lib/coq/theories/Numbers/NatInt/NZMulOrder.vo
+lib/coq/theories/Numbers/NatInt/NZOrder.vo
+lib/coq/theories/Numbers/Natural/Abstract/NAdd.vo
+lib/coq/theories/Numbers/Natural/Abstract/NAddOrder.vo
+lib/coq/theories/Numbers/Natural/Abstract/NAxioms.vo
+lib/coq/theories/Numbers/Natural/Abstract/NBase.vo
+lib/coq/theories/Numbers/Natural/Abstract/NIso.vo
+lib/coq/theories/Numbers/Natural/Abstract/NMul.vo
+lib/coq/theories/Numbers/Natural/Abstract/NMulOrder.vo
+lib/coq/theories/Numbers/Natural/Abstract/NOrder.vo
+lib/coq/theories/Numbers/Natural/Abstract/NSub.vo
+lib/coq/theories/Numbers/Natural/BigN/BigN.vo
+lib/coq/theories/Numbers/Natural/BigN/NMake.vo
+lib/coq/theories/Numbers/Natural/BigN/Nbasic.vo
+lib/coq/theories/Numbers/Natural/Binary/NBinDefs.vo
+lib/coq/theories/Numbers/Natural/Binary/NBinary.vo
+lib/coq/theories/Numbers/Natural/Peano/NPeano.vo
+lib/coq/theories/Numbers/Natural/SpecViaZ/NSig.vo
+lib/coq/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.vo
+lib/coq/theories/Numbers/NumPrelude.vo
+lib/coq/theories/Numbers/Rational/BigQ/BigQ.vo
+lib/coq/theories/Numbers/Rational/BigQ/QMake.vo
+lib/coq/theories/Numbers/Rational/SpecViaQ/QSig.vo
+lib/coq/theories/Program/Basics.vo
+lib/coq/theories/Program/Combinators.vo
+lib/coq/theories/Program/Equality.vo
+lib/coq/theories/Program/Program.vo
+lib/coq/theories/Program/Subset.vo
+lib/coq/theories/Program/Syntax.vo
+lib/coq/theories/Program/Tactics.vo
+lib/coq/theories/Program/Utils.vo
+lib/coq/theories/Program/Wf.vo
lib/coq/theories/QArith/QArith.vo
lib/coq/theories/QArith/QArith_base.vo
+lib/coq/theories/QArith/Qabs.vo
lib/coq/theories/QArith/Qcanon.vo
+lib/coq/theories/QArith/Qfield.vo
+lib/coq/theories/QArith/Qpower.vo
lib/coq/theories/QArith/Qreals.vo
lib/coq/theories/QArith/Qreduction.vo
lib/coq/theories/QArith/Qring.vo
+lib/coq/theories/QArith/Qround.vo
lib/coq/theories/Reals/Alembert.vo
lib/coq/theories/Reals/AltSeries.vo
lib/coq/theories/Reals/ArithProp.vo
@@ -250,6 +607,7 @@ lib/coq/theories/Reals/Rgeom.vo
lib/coq/theories/Reals/RiemannInt.vo
lib/coq/theories/Reals/RiemannInt_SF.vo
lib/coq/theories/Reals/Rlimit.vo
+lib/coq/theories/Reals/Rlogic.vo
lib/coq/theories/Reals/Rpow_def.vo
lib/coq/theories/Reals/Rpower.vo
lib/coq/theories/Reals/Rprod.vo
@@ -268,12 +626,10 @@ lib/coq/theories/Reals/SeqSeries.vo
lib/coq/theories/Reals/SplitAbsolu.vo
lib/coq/theories/Reals/SplitRmult.vo
lib/coq/theories/Reals/Sqrt_reg.vo
-lib/coq/theories/Relations/Newman.vo
lib/coq/theories/Relations/Operators_Properties.vo
lib/coq/theories/Relations/Relation_Definitions.vo
lib/coq/theories/Relations/Relation_Operators.vo
lib/coq/theories/Relations/Relations.vo
-lib/coq/theories/Relations/Rstar.vo
lib/coq/theories/Setoids/Setoid.vo
lib/coq/theories/Sets/Classical_sets.vo
lib/coq/theories/Sets/Constructive_sets.vo
@@ -304,6 +660,7 @@ lib/coq/theories/Sorting/Permutation.vo
lib/coq/theories/Sorting/Sorting.vo
lib/coq/theories/Strings/Ascii.vo
lib/coq/theories/Strings/String.vo
+lib/coq/theories/Unicode/Utf8.vo
lib/coq/theories/Wellfounded/Disjoint_Union.vo
lib/coq/theories/Wellfounded/Inclusion.vo
lib/coq/theories/Wellfounded/Inverse_Image.vo
@@ -319,6 +676,8 @@ lib/coq/theories/ZArith/Wf_Z.vo
lib/coq/theories/ZArith/ZArith.vo
lib/coq/theories/ZArith/ZArith_base.vo
lib/coq/theories/ZArith/ZArith_dec.vo
+lib/coq/theories/ZArith/ZOdiv.vo
+lib/coq/theories/ZArith/ZOdiv_def.vo
lib/coq/theories/ZArith/Zabs.vo
lib/coq/theories/ZArith/Zbinary.vo
lib/coq/theories/ZArith/Zbool.vo
@@ -326,6 +685,7 @@ lib/coq/theories/ZArith/Zcompare.vo
lib/coq/theories/ZArith/Zcomplements.vo
lib/coq/theories/ZArith/Zdiv.vo
lib/coq/theories/ZArith/Zeven.vo
+lib/coq/theories/ZArith/Zgcd_alt.vo
lib/coq/theories/ZArith/Zhints.vo
lib/coq/theories/ZArith/Zlogarithm.vo
lib/coq/theories/ZArith/Zmax.vo
@@ -336,24 +696,51 @@ lib/coq/theories/ZArith/Znat.vo
lib/coq/theories/ZArith/Znumtheory.vo
lib/coq/theories/ZArith/Zorder.vo
lib/coq/theories/ZArith/Zpow_def.vo
+lib/coq/theories/ZArith/Zpow_facts.vo
lib/coq/theories/ZArith/Zpower.vo
lib/coq/theories/ZArith/Zsqrt.vo
lib/coq/theories/ZArith/Zwf.vo
lib/coq/theories/ZArith/auxiliary.vo
lib/coq/tools/coqdoc/coqdoc.css
lib/coq/tools/coqdoc/coqdoc.sty
+lib/coq/toplevel/auto_ind_decl.cmi
+lib/coq/toplevel/cerrors.cmi
+lib/coq/toplevel/class.cmi
+lib/coq/toplevel/classes.cmi
+lib/coq/toplevel/command.cmi
+lib/coq/toplevel/coqinit.cmi
+lib/coq/toplevel/coqtop.cmi
+lib/coq/toplevel/discharge.cmi
+lib/coq/toplevel/himsg.cmi
+lib/coq/toplevel/ind_tables.cmi
+lib/coq/toplevel/line_oriented_parser.cmi
+lib/coq/toplevel/metasyntax.cmi
+lib/coq/toplevel/mltop.cmi
+lib/coq/toplevel/protectedtoplevel.cmi
+lib/coq/toplevel/record.cmi
+lib/coq/toplevel/toplevel.a
+lib/coq/toplevel/toplevel.cma
+lib/coq/toplevel/toplevel.cmi
+lib/coq/toplevel/toplevel.cmxa
+lib/coq/toplevel/usage.cmi
+lib/coq/toplevel/vernac.cmi
+lib/coq/toplevel/vernacentries.cmi
+lib/coq/toplevel/vernacexpr.cmi
+lib/coq/toplevel/vernacinterp.cmi
+lib/coq/toplevel/whelp.cmi
man/man1/coq-interface.1
+man/man1/coq-parser.1
man/man1/coq-tex.1
man/man1/coq_makefile.1
man/man1/coqc.1
man/man1/coqdep.1
man/man1/coqdoc.1
+man/man1/coqide.1
man/man1/coqmktop.1
man/man1/coqtop.1
man/man1/coqtop.byte.1
man/man1/coqwc.1
man/man1/gallina.1
-man/man1/parser.1
share/emacs/site-lisp/coq-inferior.el
share/emacs/site-lisp/coq.el
share/emacs/site-lisp/coqdoc.sty
diff --git a/lang/coq/PLIST.opt b/lang/coq/PLIST.opt
index 2464aadaf65..d650b8b8f3f 100644
--- a/lang/coq/PLIST.opt
+++ b/lang/coq/PLIST.opt
@@ -1,6 +1,7 @@
-@comment $NetBSD: PLIST.opt,v 1.5 2008/04/27 10:46:16 tonio Exp $
+@comment $NetBSD: PLIST.opt,v 1.6 2009/09/05 20:44:57 tonio Exp $
bin/coq-interface.opt
+bin/coq-parser.opt
+bin/coqchk.opt
${PLIST.coqide}bin/coqide.opt
bin/coqtop.opt
-bin/parser.opt
man/man1/coqtop.opt.1
diff --git a/lang/coq/distinfo b/lang/coq/distinfo
index 7ed6e1723e1..7934cf35172 100644
--- a/lang/coq/distinfo
+++ b/lang/coq/distinfo
@@ -1,7 +1,8 @@
-$NetBSD: distinfo,v 1.8 2008/01/12 11:48:40 tonio Exp $
+$NetBSD: distinfo,v 1.9 2009/09/05 20:44:58 tonio Exp $
-SHA1 (coq-8.1pl3.tar.gz) = c06141891c2a793ff6b4bc1f106d9477b3a9a52e
-RMD160 (coq-8.1pl3.tar.gz) = f8f4749e1014cb47a83915550713cf9ce1992e34
-Size (coq-8.1pl3.tar.gz) = 3003593 bytes
-SHA1 (patch-aa) = bdfe2986da84b13c7df383caf969858707be83f3
-SHA1 (patch-ab) = b252096b0bef5fee0a2f719ddc17021fd013ed64
+SHA1 (coq-8.2pl1.tar.gz) = 4aed3302adc2edbaa5d97984512c1c13014bd649
+RMD160 (coq-8.2pl1.tar.gz) = dd5758a94bb3de49967cec76baa33eb5169659ce
+Size (coq-8.2pl1.tar.gz) = 3600620 bytes
+SHA1 (patch-aa) = 2725d9fb667f6a66bf9cb6dd0bdcdbd94d8c1fd6
+SHA1 (patch-ab) = 6573a11efab6ef7c026e8fd39b23e8596dee5a61
+SHA1 (patch-ac) = 30780c9f96ad16c814a5edc50bd1edbd030aa9b5
diff --git a/lang/coq/patches/patch-aa b/lang/coq/patches/patch-aa
index 5f3afb50e2f..026e33168dd 100644
--- a/lang/coq/patches/patch-aa
+++ b/lang/coq/patches/patch-aa
@@ -1,168 +1,13 @@
-$NetBSD: patch-aa,v 1.7 2008/01/12 11:48:40 tonio Exp $
+$NetBSD: patch-aa,v 1.8 2009/09/05 20:44:58 tonio Exp $
---- Makefile.orig Mon Nov 12 16:10:25 2007
+--- Makefile.orig 2009-04-08 17:38:39.000000000 +0200
+++ Makefile
-@@ -690,22 +690,22 @@ install-coqide:: install-ide-$(HASCOQIDE
- install-ide-no:
-
- install-ide-byte:
-- $(MKDIR) $(FULLBINDIR)
-- cp $(COQIDEBYTE) $(FULLBINDIR)
-+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR)
-+ ${BSD_INSTALL_SCRIPT} $(COQIDEBYTE) $(FULLBINDIR)
- cd $(FULLBINDIR); ln -sf coqide.byte$(EXE) coqide$(EXE)
-
- install-ide-opt:
-- $(MKDIR) $(FULLBINDIR)
-- cp $(COQIDEBYTE) $(COQIDEOPT) $(FULLBINDIR)
-+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR)
-+ ${BSD_INSTALL_SCRIPT} $(COQIDEBYTE) $(COQIDEOPT) $(FULLBINDIR)
- cd $(FULLBINDIR); ln -sf coqide.opt$(EXE) coqide$(EXE)
-
- install-ide-files:
-- $(MKDIR) $(FULLIDELIB)
-- cp $(IDEFILES) $(FULLIDELIB)
-+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLIDELIB)
-+ ${BSD_INSTALL_DATA} $(IDEFILES) $(FULLIDELIB)
-
- install-ide-info:
-- $(MKDIR) $(FULLIDELIB)
-- cp ide/FAQ $(FULLIDELIB)
-+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLIDELIB)
-+ ${BSD_INSTALL_DATA} ide/FAQ $(FULLIDELIB)
-
+@@ -24,8 +24,6 @@
+ # by Emacs' next-error.
###########################################################################
- # Pcoq: special binaries for debugging (coq-interface, parser)
-@@ -775,18 +775,18 @@ clean::
- install-pcoq:: install-pcoq-binaries install-pcoq-files install-pcoq-manpages
-
- install-pcoq-binaries::
-- $(MKDIR) $(FULLBINDIR)
-- cp $(COQINTERFACE) $(FULLBINDIR)
-+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR)
-+ ${BSD_INSTALL_PROGRAM} $(COQINTERFACE) $(FULLBINDIR)
-
- install-pcoq-files::
-- $(MKDIR) $(FULLCOQLIB)/contrib/interface
-- cp $(INTERFACERC) $(FULLCOQLIB)/contrib/interface
-+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/contrib/interface
-+ ${BSD_INSTALL_DATA} $(INTERFACERC) $(FULLCOQLIB)/contrib/interface
-
- PCOQMANPAGES=man/coq-interface.1 man/parser.1
-
- install-pcoq-manpages:
-- $(MKDIR) $(FULLMANDIR)/man1
-- cp $(PCOQMANPAGES) $(FULLMANDIR)/man1
-+ ${BSD_INSTALL_DATA_DIR} $(FULLMANDIR)/man1
-+ ${BSD_INSTALL_MAN} $(PCOQMANPAGES) $(FULLMANDIR)/man1
-
- ###########################################################################
- # tests
-@@ -1244,22 +1244,21 @@ install-coqlight: install-binaries insta
- install-binaries:: install-$(BEST) install-tools
-
- install-byte::
-- $(MKDIR) $(FULLBINDIR)
-- cp $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(FULLBINDIR)
-+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR)
-+ ${BSD_INSTALL_SCRIPT} $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(FULLBINDIR)
- cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE)
-
- install-opt::
-- $(MKDIR) $(FULLBINDIR)
-- cp $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(FULLBINDIR)
-+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR)
-+ ${BSD_INSTALL_SCRIPT} $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(FULLBINDIR)
- cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE)
- install-tools::
-- $(MKDIR) $(FULLBINDIR)
- # recopie des fichiers de style pour coqide
-- $(MKDIR) $(FULLCOQLIB)/tools/coqdoc
-- touch $(FULLCOQLIB)/tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715)
-- cp tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
-- cp $(TOOLS) $(FULLBINDIR)
-+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR)
-+ ${BSD_INSTALL_SCRIPT} $(TOOLS) $(FULLBINDIR)
-+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLCOQLIB)/tools/coqdoc
-+ ${BSD_INSTALL_DATA} tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
-
- LIBFILES=$(THEORIESVO) $(CONTRIBVO)
- LIBFILESLIGHT=$(THEORIESLIGHTVO)
-@@ -1274,52 +1273,55 @@ OBJECTCMA=lib/lib.cma kernel/kernel.cma
- OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa)
-
- install-library:
-- $(MKDIR) $(FULLCOQLIB)
-+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)
- for f in $(LIBFILES); do \
-- $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \
-- cp $$f $(FULLCOQLIB)/`dirname $$f`; \
-+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/`dirname $$f`; \
-+ ${BSD_INSTALL_DATA} $$f $(FULLCOQLIB)/`dirname $$f`; \
- done
-- $(MKDIR) $(FULLCOQLIB)/states
-- cp states/*.coq $(FULLCOQLIB)/states
-- $(MKDIR) $(FULLCOQLIB)/user-contrib
-- cp $(OBJECTCMA) $(OBJECTCMXA) $(GRAMMARCMA) $(FULLCOQLIB)
-+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/states
-+ ${BSD_INSTALL_DATA} states/*.coq $(FULLCOQLIB)/states
-+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/user-contrib
-+ ${BSD_INSTALL_DATA} $(OBJECTCMA) $(OBJECTCMXA) $(FULLCOQLIB)/states
-
- install-library-light:
-- $(MKDIR) $(FULLCOQLIB)
-+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)
- for f in $(LIBFILESLIGHT); do \
-- $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \
-- cp $$f $(FULLCOQLIB)/`dirname $$f`; \
-+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/`dirname $$f`; \
-+ ${BSD_INSTALL_DATA} $$f $(FULLCOQLIB)/`dirname $$f`; \
- done
-- $(MKDIR) $(FULLCOQLIB)/states
-- cp states/*.coq $(FULLCOQLIB)/states
-+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/states
-+ ${BSD_INSTALL_DATA} states/*.coq $(FULLCOQLIB)/states
-
- install-allreals::
- for f in $(ALLREALS); do \
-- $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \
-- cp $$f $(FULLCOQLIB)/`dirname $$f`; \
-+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/`dirname $$f`; \
-+ ${BSD_INSTALL_DATA} $$f $(FULLCOQLIB)/`dirname $$f`; \
- done
-
- install-coq-info: install-coq-manpages install-emacs install-latex
-
- MANPAGES=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
-- man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \
-+ man/coqc.1 man/coqtop.1 man/coqtop.byte.1 \
- man/coqwc.1 man/coqdoc.1 \
- man/coq_makefile.1 man/coqmktop.1
-+ ifeq ($(BEST),opt)
-+ MANPAGES+=man/coqtop.opt.1
-+ endif
-
- install-coq-manpages:
-- $(MKDIR) $(FULLMANDIR)/man1
-- cp $(MANPAGES) $(FULLMANDIR)/man1
-+ ${BSD_INSTALL_DATA_DIR} $(FULLMANDIR)/man1
-+ ${BSD_INSTALL_MAN} $(MANPAGES) $(FULLMANDIR)/man1
-
- install-emacs:
-- $(MKDIR) $(FULLEMACSLIB)
-- cp tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB)
-+ ${BSD_INSTALL_DATA_DIR} $(FULLEMACSLIB)
-+ ${BSD_INSTALL_DATA} tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB)
-
- # command to update TeX' kpathsea database
- #UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null
-
- install-latex:
-- $(MKDIR) $(FULLCOQDOCDIR)
-- cp tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)
-+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQDOCDIR)
-+ ${BSD_INSTALL_DATA} tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)
- # -$(UPDATETEX)
-
- ###########################################################################
+-export SHELL:=/bin/bash
+-
+ export FIND_VCS_CLAUSE:='(' \
+ -name '{arch}' -o \
+ -name '.svn' -o \
diff --git a/lang/coq/patches/patch-ab b/lang/coq/patches/patch-ab
index 60630877b49..0ed17e25bef 100644
--- a/lang/coq/patches/patch-ab
+++ b/lang/coq/patches/patch-ab
@@ -1,13 +1,22 @@
-$NetBSD: patch-ab,v 1.1 2007/12/01 13:05:37 tonio Exp $
+$NetBSD: patch-ab,v 1.2 2009/09/05 20:44:58 tonio Exp $
---- configure.orig Thu Oct 11 15:13:51 2007
+--- configure.orig 2009-07-01 11:58:00.000000000 +0200
+++ configure
-@@ -326,7 +326,7 @@ esac
+@@ -331,7 +331,7 @@ if [ "$MAKE" != "" ]; then
+ OK="no"
+ if [ -x ./make ]; then
+ MAKEVERSION=`./make -v | head -1`
+- if [ "$MAKEVERSION" == "GNU Make 3.81" ]; then OK="yes"; fi
++ if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi
+ fi
+ if [ $OK = "no" ]; then
+ echo "GNU Make >= 3.81 is needed"
+@@ -412,7 +412,7 @@ esac
# this fixes a camlp4 bug under FreeBSD
# ("native-code program cannot do a dynamic load")
-if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi
+#if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi
- CAMLVERSION=`"$bytecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
+ CAMLVERSION=`"$bytecamlc" -version`
diff --git a/lang/coq/patches/patch-ac b/lang/coq/patches/patch-ac
new file mode 100644
index 00000000000..1ac85f2dfb2
--- /dev/null
+++ b/lang/coq/patches/patch-ac
@@ -0,0 +1,12 @@
+$NetBSD: patch-ac,v 1.1 2009/09/05 20:44:58 tonio Exp $
+
+--- Makefile.stage1.orig 2009-04-08 17:38:39.000000000 +0200
++++ Makefile.stage1
+@@ -6,7 +6,6 @@
+ # # GNU Lesser General Public License Version 2.1 #
+ #######################################################################
+
+-export SHELL:=/bin/bash
+ include Makefile.build
+
+ # All includes must be declared secondary, otherwise make will delete