6f37dbf143
Main changes: Includes a new tactic (nsatz, standing for Hilbert's NullStellensatz, that extends ring to systems of polynomial equations) and a few new libraries (a certification of mergesort, a new library of finite sets with computational and logical contents separated). This version also comes with many improvements of existing features, especially regarding the tactics, the module system, extraction, the type classes, the program command, libraries, coqdoc. Here is an excerpt: * new operator <+ for conveniently chaining application of functors * new round of extension of the modular library of arithmetic * support for matching terms with binders in Ltac, * linking notations in coqdoc, * quote tactic now working on arbitrary expressions, * Lemma and co accept parameters that are automatically introduced, * interactive proofs in module types, * a beautifying coqc option for pretty-printing files See the file CHANGES for a full log of changes.
52 lines
1.8 KiB
Text
52 lines
1.8 KiB
Text
$NetBSD: patch-ab,v 1.4 2010/11/14 20:53:03 tonio Exp $
|
|
|
|
Fix mixed implicit and normal rules
|
|
This fixes build with GNU Make 3.82. See threads:
|
|
https://sympa-roc.inria.fr/wws/arc/coqdev/2010-10/msg00025.html
|
|
http://thread.gmane.org/gmane.comp.gnu.make.bugs/4912
|
|
|
|
Patch from https://gforge.inria.fr/scm/viewvc.php?diff_format=s&view=rev&root=coq&sortby=file&revision=13566
|
|
|
|
--- Makefile.common.orig 2010-06-23 13:17:17.000000000 +0000
|
|
+++ Makefile.common
|
|
@@ -365,7 +365,7 @@ DATE=$(shell LANG=C date +"%B %Y")
|
|
|
|
SOURCEDOCDIR=dev/source-doc
|
|
|
|
-CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
|
|
+CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.o %.cmi %.cma %.cmxa %.a %.cmxs %.dep.ps %.dot
|
|
|
|
### Targets forwarded by Makefile to a specific stage:
|
|
|
|
@@ -374,10 +374,12 @@ CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi
|
|
STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \
|
|
$(GENFILES) \
|
|
source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \
|
|
- $(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o
|
|
+ $(STAGE1_ML4:.ml4=.ml4-preprocessed)
|
|
+
|
|
+STAGE1_IMPLICITS:=
|
|
|
|
ifdef CM_STAGE1
|
|
- STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS)
|
|
+ STAGE1_IMPLICITS+=$(CAML_OBJECT_PATTERNS)
|
|
endif
|
|
|
|
## Enumeration of targets that require being done at stage2
|
|
@@ -402,12 +404,13 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kerne
|
|
printers debug initplugins plugins \
|
|
world install coqide coqide-files coq coqlib \
|
|
coqlight states check init theories theories-light \
|
|
- $(DOC_TARGETS) $(VO_TARGETS) validate \
|
|
- %.vo %.glob states/% install-% %.ml4-preprocessed \
|
|
+ $(DOC_TARGETS) $(VO_TARGETS) validate
|
|
+
|
|
+STAGE2_IMPLICITS:= %.vo %.glob states/% install-% %.ml4-preprocessed \
|
|
$(DOC_TARGET_PATTERNS)
|
|
|
|
ifndef CM_STAGE1
|
|
- STAGE2_TARGETS+=$(CAML_OBJECT_PATTERNS)
|
|
+ STAGE2_IMPLICITS+=$(CAML_OBJECT_PATTERNS)
|
|
endif
|
|
|
|
|