New upstream release, update changelog

5 files changed, 6 insertions, 269 deletions

diff --git a/debian/changelog b/debian/changelog
index 593104db..47377d58 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,6 +1,10 @@
-coq (8.3+dfsg-2) UNRELEASED; urgency=low
+coq (8.3.pl1+dfsg-1) UNRELEASED; urgency=low
 
-  * NOT RELEASED YET
+  * New upstream release
+    - remove all patches (applied upstream)
+  * debian/rules:
+    - run test-suite in override_dh_auto_test, skip coqchk run
+    - make "build" explicitly a phony target
 
  -- Stéphane Glondu <glondu@debian.org>  Tue, 19 Oct 2010 12:10:18 +0200
 
diff --git a/debian/patches/0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch b/debian/patches/0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch
deleted file mode 100644
index c3092bac..00000000
--- a/debian/patches/0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch
+++ /dev/null
@@ -1,23 +0,0 @@
-From: Stephane Glondu <steph@glondu.net>
-Date: Fri, 15 Oct 2010 17:24:18 +0200
-Subject: [PATCH] Fix missing -coqlib argument to coqdep in test-suite
-
-Signed-off-by: Stephane Glondu <steph@glondu.net>
----
- test-suite/Makefile |    2 +-
- 1 files changed, 1 insertions(+), 1 deletions(-)
-
-diff --git a/test-suite/Makefile b/test-suite/Makefile
-index 62d443d..98bab43 100644
---- a/test-suite/Makefile
-+++ b/test-suite/Makefile
-@@ -40,7 +40,7 @@ endif
- 
- command := $(coqtop) -top Top -load-vernac-source
- coqc := $(coqtop) -compile
--coqdep := $(BIN)coqdep
-+coqdep := $(BIN)coqdep -coqlib $(LIB)
- 
- SHOW := $(if $(VERBOSE),@true,@echo)
- HIDE := $(if $(VERBOSE),,@)
--- 
diff --git a/debian/patches/0002-Fix-mixed-implicit-and-normal-rules.patch b/debian/patches/0002-Fix-mixed-implicit-and-normal-rules.patch
deleted file mode 100644
index 79c1a22b..00000000
--- a/debian/patches/0002-Fix-mixed-implicit-and-normal-rules.patch
+++ /dev/null
@@ -1,85 +0,0 @@
-From: Stephane Glondu <steph@glondu.net>
-Date: Tue, 19 Oct 2010 12:00:55 +0200
-Subject: [PATCH] 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
-
-Signed-off-by: Stephane Glondu <steph@glondu.net>
----
- Makefile        |   10 ++++++++++
- Makefile.common |   15 +++++++++------
- 2 files changed, 19 insertions(+), 6 deletions(-)
-
-diff --git a/Makefile b/Makefile
-index 975ece0..908dbd6 100644
---- a/Makefile
-+++ b/Makefile
-@@ -160,9 +160,19 @@ else
- stage1 $(STAGE1_TARGETS) : always
- 	$(call stage-template,1)
- 
-+ifneq (,$(STAGE1_IMPLICITS))
-+$(STAGE1_IMPLICITS) : always
-+	$(call stage-template,1)
-+endif
-+
- stage2 $(STAGE2_TARGETS) : stage1
- 	$(call stage-template,2)
- 
-+ifneq (,$(STAGE2_IMPLICITS))
-+$(STAGE2_IMPLICITS) : stage1
-+	$(call stage-template,2)
-+endif
-+
- # Nota:
- # - world is one of the targets in $(STAGE2_TARGETS), hence launching
- # "make" or "make world" leads to recursion into stage1 then stage2
-diff --git a/Makefile.common b/Makefile.common
-index cc38980..46bf217 100644
---- a/Makefile.common
-+++ b/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 %.cma %.cmxa %.cmxs %.dep.ps %.dot
- 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 kernel byterun library proofs tactics \
-   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
- 
- 
--- 
diff --git a/debian/patches/0003-Support-for-camlp5-6.02.1.patch b/debian/patches/0003-Support-for-camlp5-6.02.1.patch
deleted file mode 100644
index 4dfaa7b9..00000000
--- a/debian/patches/0003-Support-for-camlp5-6.02.1.patch
+++ /dev/null
@@ -1,156 +0,0 @@
-From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Date: Tue, 16 Nov 2010 20:25:56 +0000
-Subject: [PATCH] Support for camlp5 6.02.1
-
-Signed-off-by: Stephane Glondu <steph@glondu.net>
----
- lib/compat.ml4         |   12 ++++++++++++
- parsing/pcoq.ml4       |   23 ++++++++++++++---------
- parsing/pcoq.mli       |    2 ++
- toplevel/metasyntax.ml |   26 +++++++++++++-------------
- 4 files changed, 41 insertions(+), 22 deletions(-)
-
-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 90a9220..de1b3ed 100644
---- a/parsing/pcoq.ml4
-+++ b/parsing/pcoq.ml4
-@@ -145,6 +145,11 @@ module Gram =
-       G.delete_rule e pil
-   end
- 
-+IFDEF CAMLP5_6_02_1 THEN
-+let entry_print x = Gram.Entry.print !Pp_control.std_ft x
-+ELSE
-+let entry_print = Gram.Entry.print
-+END
- 
- let camlp4_verbosity silent f x =
-   let a = !Gramext.warning_verbose in
-@@ -631,16 +636,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 +659,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
-diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
-index e4566e7..7dbd78e 100644
---- a/parsing/pcoq.mli
-+++ b/parsing/pcoq.mli
-@@ -23,6 +23,8 @@ open Libnames
- 
- module Gram : Grammar.S with type te = Compat.token
- 
-+val entry_print : 'a Gram.Entry.e -> unit
-+
- (**********************************************************************)
- (* The parser of Coq is built from three kinds of rule declarations:
-    - dynamic rules declared at the evaluation of Coq files (using
-diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
-index 6ee00f4..ddb1b11 100644
---- a/toplevel/metasyntax.ml
-+++ b/toplevel/metasyntax.ml
-@@ -106,33 +106,33 @@ let add_tactic_notation (n,prods,e) =
- let print_grammar = function
-   | "constr" | "operconstr" | "binder_constr" ->
-       msgnl (str "Entry constr is");
--      Gram.Entry.print Pcoq.Constr.constr;
-+      entry_print Pcoq.Constr.constr;
-       msgnl (str "and lconstr is");
--      Gram.Entry.print Pcoq.Constr.lconstr;
-+      entry_print Pcoq.Constr.lconstr;
-       msgnl (str "where binder_constr is");
--      Gram.Entry.print Pcoq.Constr.binder_constr;
-+      entry_print Pcoq.Constr.binder_constr;
-       msgnl (str "and operconstr is");
--      Gram.Entry.print Pcoq.Constr.operconstr;
-+      entry_print Pcoq.Constr.operconstr;
-   | "pattern" ->
--      Gram.Entry.print Pcoq.Constr.pattern
-+      entry_print Pcoq.Constr.pattern
-   | "tactic" ->
-       msgnl (str "Entry tactic_expr is");
--      Gram.Entry.print Pcoq.Tactic.tactic_expr;
-+      entry_print Pcoq.Tactic.tactic_expr;
-       msgnl (str "Entry binder_tactic is");
--      Gram.Entry.print Pcoq.Tactic.binder_tactic;
-+      entry_print Pcoq.Tactic.binder_tactic;
-       msgnl (str "Entry simple_tactic is");
--      Gram.Entry.print Pcoq.Tactic.simple_tactic;
-+      entry_print Pcoq.Tactic.simple_tactic;
-   | "vernac" ->
-       msgnl (str "Entry vernac is");
--      Gram.Entry.print Pcoq.Vernac_.vernac;
-+      entry_print Pcoq.Vernac_.vernac;
-       msgnl (str "Entry command is");
--      Gram.Entry.print Pcoq.Vernac_.command;
-+      entry_print Pcoq.Vernac_.command;
-       msgnl (str "Entry syntax is");
--      Gram.Entry.print Pcoq.Vernac_.syntax;
-+      entry_print Pcoq.Vernac_.syntax;
-       msgnl (str "Entry gallina is");
--      Gram.Entry.print Pcoq.Vernac_.gallina;
-+      entry_print Pcoq.Vernac_.gallina;
-       msgnl (str "Entry gallina_ext is");
--      Gram.Entry.print Pcoq.Vernac_.gallina_ext;
-+      entry_print Pcoq.Vernac_.gallina_ext;
-   | _ -> error "Unknown or unprintable grammar entry."
- 
- (**********************************************************************)
--- 
diff --git a/debian/patches/series b/debian/patches/series
deleted file mode 100644
index de7a4950..00000000
--- a/debian/patches/series
+++ /dev/null
@@ -1,3 +0,0 @@
-0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch
-0002-Fix-mixed-implicit-and-normal-rules.patch
-0003-Support-for-camlp5-6.02.1.patch