summaryrefslogtreecommitdiff
path: root/debian/patches
diff options
context:
space:
mode:
Diffstat (limited to 'debian/patches')
-rw-r--r--debian/patches/00list7
-rwxr-xr-xdebian/patches/browser.dpatch19
-rwxr-xr-xdebian/patches/camlp5.dpatch563
-rwxr-xr-xdebian/patches/cmxa-install.dpatch23
-rwxr-xr-xdebian/patches/configure.dpatch19
-rwxr-xr-xdebian/patches/coqdoc_stdlib.dpatch19
-rwxr-xr-xdebian/patches/makefile.dpatch20
-rw-r--r--debian/patches/no-complexity-test.dpatch21
8 files changed, 691 insertions, 0 deletions
diff --git a/debian/patches/00list b/debian/patches/00list
new file mode 100644
index 00000000..333bbd2f
--- /dev/null
+++ b/debian/patches/00list
@@ -0,0 +1,7 @@
+camlp5
+coqdoc_stdlib
+browser
+makefile
+no-complexity-test
+configure
+cmxa-install
diff --git a/debian/patches/browser.dpatch b/debian/patches/browser.dpatch
new file mode 100755
index 00000000..ba55f3de
--- /dev/null
+++ b/debian/patches/browser.dpatch
@@ -0,0 +1,19 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## browser.dpatch by Samuel Mimram <smimram@debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Use the default Debian browser for help.
+
+@DPATCH@
+diff -urNad coq-8.0pl3+8.1alpha~/lib/options.ml coq-8.0pl3+8.1alpha/lib/options.ml
+--- coq-8.0pl3+8.1alpha~/lib/options.ml 2005-12-26 20:07:21.000000000 +0000
++++ coq-8.0pl3+8.1alpha/lib/options.ml 2006-04-29 16:06:20.000000000 +0000
+@@ -117,7 +117,4 @@
+ "\" must contain exactly one placeholder \"%s\".")
+ else pre,post
+ with
+- Not_found ->
+- if Sys.os_type = "Win32"
+- then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", ""
+- else "netscape -remote \"OpenURL(", ")\""
++ Not_found -> "/usr/bin/x-www-browser ", ""
diff --git a/debian/patches/camlp5.dpatch b/debian/patches/camlp5.dpatch
new file mode 100755
index 00000000..2c5b8643
--- /dev/null
+++ b/debian/patches/camlp5.dpatch
@@ -0,0 +1,563 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## camlp5.dpatch by Samuel Mimram <smimram@debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Use camlp5 instead of the new camlp4 for coq.
+
+@DPATCH@
+diff -urNad coq-8.1.pl1+dfsg~/Makefile coq-8.1.pl1+dfsg/Makefile
+--- coq-8.1.pl1+dfsg~/Makefile 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/Makefile 2007-08-24 10:56:52.000000000 +0000
+@@ -1504,11 +1504,11 @@
+
+ # BEFOREDEPEND+= parsing/pcoq.ml parsing/extend.ml
+
+-# File using pa_ifdef and only necessary for parsing ml files
++# File using pa_macro and only necessary for parsing ml files
+
+ parsing/q_coqast.cmo: parsing/q_coqast.ml4
+ $(SHOW)'OCAMLC4 $<'
+- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo $(CAMLP4COMPAT) -impl" -c -impl $<
++ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo $(CAMLP4COMPAT) -impl" -c -impl $<
+
+ # toplevel/mltop.ml4 (ifdef Byte)
+
+@@ -1522,11 +1522,11 @@
+
+ toplevel/mltop.byteml: toplevel/mltop.ml4
+ $(SHOW)'CAMLP4O $<'
+- $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo -DByte -impl $< > $@ || rm -f $@
++ $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo pr_o.cmo -DByte -impl $< > $@ || rm -f $@
+
+ toplevel/mltop.optml: toplevel/mltop.ml4
+ $(SHOW)'CAMLP4O $<'
+- $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo -impl $< > $@ || rm -f $@
++ $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo pr_o.cmo -impl $< > $@ || rm -f $@
+
+ ML4FILES += toplevel/mltop.ml4
+
+@@ -1571,11 +1571,11 @@
+
+ lib/compat.cmo: lib/compat.ml4
+ $(SHOW)'OCAMLC4 $<'
+- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo -impl" -c -impl $<
++ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo -impl" -c -impl $<
+
+ lib/compat.cmx: lib/compat.ml4
+ $(SHOW)'OCAMLOPT $<'
+- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo -impl" -c -impl $<
++ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo -impl" -c -impl $<
+
+ # files compiled with camlp4 because of streams syntax
+
+@@ -1654,7 +1654,7 @@
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
+
+ %.ml: %.ml4
+- $(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@
++ $(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@
+
+ #.v.vo:
+ # $(BOOTCOQTOP) -compile $*
+diff -urNad coq-8.1.pl1+dfsg~/Makefile.dep coq-8.1.pl1+dfsg/Makefile.dep
+--- coq-8.1.pl1+dfsg~/Makefile.dep 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/Makefile.dep 2007-08-24 10:56:52.000000000 +0000
+@@ -12,4 +12,4 @@
+ include .depend.camlp4
+
+ .ml4.ml:
+- $(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@
++ $(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@
+diff -urNad coq-8.1.pl1+dfsg~/config/Makefile.template coq-8.1.pl1+dfsg/config/Makefile.template
+--- coq-8.1.pl1+dfsg~/config/Makefile.template 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/config/Makefile.template 2007-08-24 10:56:52.000000000 +0000
+@@ -62,7 +62,7 @@
+ CAMLMKTOP="CAMLMKTOPEXEC"
+
+ # Caml flags
+-CAMLFLAGS=CAMLANNOTATEFLAG
++CAMLFLAGS=-rectypes CAMLANNOTATEFLAG
+
+ # Compilation debug flag
+ CAMLDEBUG=COQDEBUGFLAG
+@@ -80,8 +80,8 @@
+ BEST=BESTCOMPILER
+
+ # For Camlp4 use
+-P4=$(COQTOP)/bin/$(ARCH)/call_camlp4 -I $(COQTOP)/src/parsing
+-P4DEP=$(COQTOP)/bin/$(ARCH)/camlp4dep
++P4=$(COQTOP)/bin/$(ARCH)/call_camlp5 -I $(COQTOP)/src/parsing
++P4DEP=$(COQTOP)/bin/$(ARCH)/camlp5dep
+
+ # Your architecture
+ # Can be obtain by UNIX command arch
+diff -urNad coq-8.1.pl1+dfsg~/configure coq-8.1.pl1+dfsg/configure
+--- coq-8.1.pl1+dfsg~/configure 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/configure 2007-08-24 10:56:52.000000000 +0000
+@@ -78,7 +78,7 @@
+ ocamllexexec=ocamllex
+ ocamlyaccexec=ocamlyacc
+ ocamlmktopexec=ocamlmktop
+-camlp4oexec=camlp4o
++camlp4oexec=camlp5o
+
+
+ coq_debug_flag=
+@@ -153,7 +153,7 @@
+ arch=$2
+ shift;;
+ -opt|--opt) bytecamlc=ocamlc.opt
+- camlp4oexec=camlp4o # can't add .opt since dyn load'll be required
++ camlp4oexec=camlp5o # can't add .opt since dyn load'll be required
+ nativecamlc=ocamlopt.opt;;
+ -fsets|--fsets) fsets_opt=yes
+ case "$2" in
+@@ -297,7 +297,7 @@
+ ocamllexexec=$CAMLBIN/ocamllex
+ ocamlyaccexec=$CAMLBIN/ocamlyacc
+ camlmktopexec=$CAMLBIN/ocamlmktop
+- camlp4oexec=$CAMLBIN/camlp4o
++ camlp4oexec=$CAMLBIN/camlp5o
+ esac
+
+ if test ! -f "$CAMLC" ; then
+@@ -362,10 +362,10 @@
+
+ #case $OS in
+ # Win32)
+- CAMLP4LIB=+camlp4
++ CAMLP4LIB=+camlp5
+ # ;;
+ # *)
+-# CAMLP4LIB=${CAMLLIB}/camlp4
++# CAMLP4LIB=${CAMLLIB}/camlp5
+ #esac
+
+ # OS dependent libraries
+@@ -615,7 +615,7 @@
+ ESCLIBDIR="`VAR=LIBDIR escape_var`"
+ ESCCAMLDIR="`VAR=CAMLBIN escape_var`"
+ ESCCAMLLIB="`VAR=CAMLLIB escape_var`"
+-ESCCAMLP4LIB="$ESCCAMLLIB"/camlp4
++ESCCAMLP4LIB="$ESCCAMLLIB"/camlp5
+
+ mlconfig_file="$COQSRC/config/coq_config.ml"
+ rm -f $mlconfig_file
+@@ -739,8 +739,8 @@
+
+ if test "$coq_debug_flag" = "-g" ; then
+ rm -f $OCAMLDEBUGCOQ
+- if [ "$CAMLP4LIB" = "+camlp4" ] ; then
+- CAMLP4LIBFORCAMLDEBUG=$CAMLLIB/camlp4
++ if [ "$CAMLP4LIB" = "+camlp5" ] ; then
++ CAMLP4LIBFORCAMLDEBUG=$CAMLLIB/camlp5
+ else
+ CAMLP4LIBFORCAMLDEBUG=$CAMLP4LIB
+ fi
+diff -urNad coq-8.1.pl1+dfsg~/dev/ocamldebug-coq.template coq-8.1.pl1+dfsg/dev/ocamldebug-coq.template
+--- coq-8.1.pl1+dfsg~/dev/ocamldebug-coq.template 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/dev/ocamldebug-coq.template 2007-08-24 10:56:52.000000000 +0000
+@@ -7,7 +7,7 @@
+ export COQTH=$COQLIB/theories
+ CAMLBIN=CAMLBINDIRECTORY
+ OCAMLDEBUG=$CAMLBIN/ocamldebug
+-export CAMLP4LIB=`$CAMLBIN/camlp4 -where`
++export CAMLP4LIB=`$CAMLBIN/camlp5 -where`
+
+ exec $OCAMLDEBUG \
+ -I $CAMLP4LIB \
+diff -urNad coq-8.1.pl1+dfsg~/lib/compat.ml4 coq-8.1.pl1+dfsg/lib/compat.ml4
+--- coq-8.1.pl1+dfsg~/lib/compat.ml4 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/lib/compat.ml4 2007-08-24 10:56:52.000000000 +0000
+@@ -11,6 +11,7 @@
+ (* IFDEF not available in 3.06; use ifdef instead *)
+
+ (* type loc is different in 3.08 *)
++(*
+ ifdef OCAML_308 then
+ module M = struct
+ type loc = Token.flocation
+@@ -32,8 +33,9 @@
+ let make_loc x = x
+ let unloc x = x
+ end
++*)
+
+-type loc = M.loc
+-let dummy_loc = M.dummy_loc
+-let unloc = M.unloc
+-let make_loc = M.make_loc
++type loc = Stdpp.location
++let dummy_loc = Stdpp.dummy_loc
++let make_loc = Stdpp.make_loc
++let unloc loc = Stdpp.first_pos loc, Stdpp.last_pos loc
+diff -urNad coq-8.1.pl1+dfsg~/lib/util.ml coq-8.1.pl1+dfsg/lib/util.ml
+--- coq-8.1.pl1+dfsg~/lib/util.ml 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/lib/util.ml 2007-08-24 10:56:52.000000000 +0000
+@@ -34,7 +34,7 @@
+ let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s)
+ let join_loc loc1 loc2 =
+ if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
+- else (fst loc1, snd loc2)
++ else Stdpp.encl_loc loc1 loc2
+
+ (* Like Exc_located, but specifies the outermost file read, the filename
+ associated to the location of the error, and the error itself. *)
+diff -urNad coq-8.1.pl1+dfsg~/parsing/argextend.ml4 coq-8.1.pl1+dfsg/parsing/argextend.ml4
+--- coq-8.1.pl1+dfsg~/parsing/argextend.ml4 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/argextend.ml4 2007-08-24 10:56:52.000000000 +0000
+@@ -12,7 +12,7 @@
+ open Q_util
+ open Q_coqast
+
+-let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
++let join_loc = Util.join_loc
+ let loc = Util.dummy_loc
+ let default_loc = <:expr< Util.dummy_loc >>
+
+@@ -226,7 +226,7 @@
+ let t, g = interp_entry_name loc e sep in (g, Some (s,t))
+ | s = STRING ->
+ if String.length s > 0 && Util.is_letter s.[0] then
+- Pcoq.lexer.Token.using ("", s);
++ Pcoq.lexer.Token.tok_using ("", s);
+ (<:expr< (Gramext.Stoken (Lexer.terminal $str:s$)) >>, None)
+ ] ]
+ ;
+diff -urNad coq-8.1.pl1+dfsg~/parsing/egrammar.mli coq-8.1.pl1+dfsg/parsing/egrammar.mli
+--- coq-8.1.pl1+dfsg~/parsing/egrammar.mli 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/egrammar.mli 2007-08-24 10:56:52.000000000 +0000
+@@ -45,7 +45,7 @@
+ type grammar_tactic_production =
+ | TacTerm of string
+ | TacNonTerm of
+- loc * (Token.t Gramext.g_symbol * Genarg.argument_type) * string option
++ loc * ((string * string) Gramext.g_symbol * Genarg.argument_type) * string option
+
+ val extend_tactic_grammar :
+ string -> grammar_tactic_production list list -> unit
+@@ -61,7 +61,7 @@
+ (*
+ val reset_extend_grammars_v8 : unit -> unit
+ *)
+-val interp_entry_name : int -> string -> entry_type * Token.t Gramext.g_symbol
++val interp_entry_name : int -> string -> entry_type * (string * string) Gramext.g_symbol
+
+ val recover_notation_grammar :
+ notation -> (precedence * tolerability list) -> notation_grammar
+diff -urNad coq-8.1.pl1+dfsg~/parsing/pcoq.ml4 coq-8.1.pl1+dfsg/parsing/pcoq.ml4
+--- coq-8.1.pl1+dfsg~/parsing/pcoq.ml4 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/pcoq.ml4 2007-08-24 10:56:52.000000000 +0000
+@@ -30,20 +30,23 @@
+ lexer. B.B. *)
+
+ let lexer = {
+- Token.func = Lexer.func;
+- Token.using = Lexer.add_token;
+- Token.removing = (fun _ -> ());
+- Token.tparse = Lexer.tparse;
+- Token.text = Lexer.token_text }
++ Token.tok_func = Lexer.func;
++ Token.tok_using = Lexer.add_token;
++ Token.tok_removing = (fun _ -> ());
++ Token.tok_match = Token.default_match;
++ (* Token.parse = Lexer.tparse; *)
++ Token.tok_comm = None;
++ Token.tok_text = Lexer.token_text }
+
+ module L =
+ struct
++ type te = string * string
+ let lexer = lexer
+ end
+
+ (* The parser of Coq *)
+
+-module G = Grammar.Make(L)
++module G = Grammar.GMake(L)
+
+ let grammar_delete e rls =
+ List.iter
+@@ -95,7 +98,7 @@
+ | ByGrammar of
+ grammar_object G.Entry.e * Gramext.position option *
+ (string option * Gramext.g_assoc option *
+- (Token.t Gramext.g_symbol list * Gramext.g_action) list) list
++ ((string * string) Gramext.g_symbol list * Gramext.g_action) list) list
+ | ByGEXTEND of (unit -> unit) * (unit -> unit)
+
+ let camlp4_state = ref []
+diff -urNad coq-8.1.pl1+dfsg~/parsing/pcoq.mli coq-8.1.pl1+dfsg/parsing/pcoq.mli
+--- coq-8.1.pl1+dfsg~/parsing/pcoq.mli 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/pcoq.mli 2007-08-24 10:56:52.000000000 +0000
+@@ -20,9 +20,9 @@
+
+ (* The lexer and parser of Coq. *)
+
+-val lexer : Token.lexer
++val lexer : (string * string) Token.glexer
+
+-module Gram : Grammar.S with type te = Token.t
++module Gram : Grammar.S with type te = (string * string)
+
+ (* The superclass of all grammar entries *)
+ type grammar_object
+@@ -42,7 +42,7 @@
+ val grammar_extend :
+ grammar_object Gram.Entry.e -> Gramext.position option ->
+ (string option * Gramext.g_assoc option *
+- (Token.t Gramext.g_symbol list * Gramext.g_action) list) list
++ ((string * string) Gramext.g_symbol list * Gramext.g_action) list) list
+ -> unit
+
+ val remove_grammars : int -> unit
+@@ -210,7 +210,7 @@
+ (* Binding entry names to campl4 entries *)
+
+ val symbol_of_production : Gramext.g_assoc option -> constr_entry ->
+- bool -> constr_production_entry -> Token.t Gramext.g_symbol
++ bool -> constr_production_entry -> (string * string) Gramext.g_symbol
+
+ (* Registering/resetting the level of an entry *)
+
+diff -urNad coq-8.1.pl1+dfsg~/parsing/ppconstr.ml coq-8.1.pl1+dfsg/parsing/ppconstr.ml
+--- coq-8.1.pl1+dfsg~/parsing/ppconstr.ml 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/ppconstr.ml 2007-08-24 10:56:52.000000000 +0000
+@@ -95,9 +95,9 @@
+ let pr_delimiters key strm =
+ strm ++ str ("%"^key)
+
+-let pr_located pr ((b,e),x) =
+- if Options.do_translate() && (b,e)<>dummy_loc then
+- let (b,e) = unloc (b,e) in
++let pr_located pr (loc,x) =
++ if Options.do_translate() && loc<>dummy_loc then
++ let (b,e) = unloc loc in
+ comment b ++ pr x ++ comment e
+ else pr x
+
+@@ -142,7 +142,7 @@
+ | CHole _ -> mt ()
+ | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
+
+-let pr_lident (b,_ as loc,id) =
++let pr_lident (loc,id) =
+ if loc <> dummy_loc then
+ let (b,_) = unloc loc in
+ pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
+diff -urNad coq-8.1.pl1+dfsg~/parsing/ppvernac.ml coq-8.1.pl1+dfsg/parsing/ppvernac.ml
+--- coq-8.1.pl1+dfsg~/parsing/ppvernac.ml 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/ppvernac.ml 2007-08-24 10:56:52.000000000 +0000
+@@ -28,7 +28,7 @@
+
+ let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
+
+-let pr_lident (b,_ as loc,id) =
++let pr_lident (loc,id) =
+ if loc <> dummy_loc then
+ let (b,_) = unloc loc in
+ pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
+@@ -39,7 +39,7 @@
+
+ let pr_fqid fqid = str (string_of_fqid fqid)
+
+-let pr_lfqid (_,_ as loc,fqid) =
++let pr_lfqid (loc,fqid) =
+ if loc <> dummy_loc then
+ let (b,_) = unloc loc in
+ pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid)
+diff -urNad coq-8.1.pl1+dfsg~/parsing/q_coqast.ml4 coq-8.1.pl1+dfsg/parsing/q_coqast.ml4
+--- coq-8.1.pl1+dfsg~/parsing/q_coqast.ml4 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/q_coqast.ml4 2007-08-24 10:56:52.000000000 +0000
+@@ -22,10 +22,8 @@
+ let anti loc x =
+ let e =
+ let loc =
+- ifdef OCAML_308 then
+- loc
+- else
+- (1, snd loc - fst loc)
++ loc
++ (* (1, snd loc - fst loc) *)
+ in <:expr< $lid:purge_str x$ >>
+ in
+ <:expr< $anti:e$ >>
+diff -urNad coq-8.1.pl1+dfsg~/parsing/q_util.ml4 coq-8.1.pl1+dfsg/parsing/q_util.ml4
+--- coq-8.1.pl1+dfsg~/parsing/q_util.ml4 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/q_util.ml4 2007-08-24 10:56:52.000000000 +0000
+@@ -37,18 +37,18 @@
+ List.fold_right
+ (fun e1 e2 ->
+ let e1 = f e1 in
+- let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in
++ let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
+ <:expr< [$e1$ :: $e2$] >>)
+ l (let loc = dummy_loc in <:expr< [] >>)
+
+ let mlexpr_of_pair m1 m2 (a1,a2) =
+ let e1 = m1 a1 and e2 = m2 a2 in
+- let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in
++ let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
+ <:expr< ($e1$, $e2$) >>
+
+ let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)=
+ let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 in
+- let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e3)) in
++ let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in
+ <:expr< ($e1$, $e2$, $e3$) >>
+
+ (* We don't give location for tactic quotation! *)
+diff -urNad coq-8.1.pl1+dfsg~/parsing/tacextend.ml4 coq-8.1.pl1+dfsg/parsing/tacextend.ml4
+--- coq-8.1.pl1+dfsg~/parsing/tacextend.ml4 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/tacextend.ml4 2007-08-24 10:56:52.000000000 +0000
+@@ -13,7 +13,7 @@
+ open Q_coqast
+ open Argextend
+
+-let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
++let join_loc = Util.join_loc
+ let loc = Util.dummy_loc
+ let default_loc = <:expr< Util.dummy_loc >>
+
+diff -urNad coq-8.1.pl1+dfsg~/parsing/vernacextend.ml4 coq-8.1.pl1+dfsg/parsing/vernacextend.ml4
+--- coq-8.1.pl1+dfsg~/parsing/vernacextend.ml4 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/vernacextend.ml4 2007-08-24 10:56:52.000000000 +0000
+@@ -13,7 +13,7 @@
+ open Q_coqast
+ open Argextend
+
+-let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
++let join_loc = Util.join_loc
+ let loc = Util.dummy_loc
+ let default_loc = <:expr< Util.dummy_loc >>
+
+diff -urNad coq-8.1.pl1+dfsg~/scripts/coqmktop.ml coq-8.1.pl1+dfsg/scripts/coqmktop.ml
+--- coq-8.1.pl1+dfsg~/scripts/coqmktop.ml 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/scripts/coqmktop.ml 2007-08-24 10:57:13.000000000 +0000
+@@ -32,7 +32,7 @@
+
+ (* 3. Toplevel objects *)
+ let camlp4topobjs =
+- ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"]
++ ["camlp5_top.cma"; "camlp5o.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"]
+ let topobjs = camlp4topobjs
+
+ let gramobjs = []
+@@ -285,12 +285,12 @@
+ (* native code *)
+ if !top then failwith "no custom toplevel in native code !";
+ let ocamloptexec = Filename.concat Coq_config.camldir "ocamlopt" in
+- (if !caml_inline_0 then ocamloptexec^" -linkall"^" -inline 0" else ocamloptexec^" -linkall")
++ (if !caml_inline_0 then ocamloptexec^" -linkall -rectypes"^" -inline 0" else ocamloptexec^" -linkall -rectypes")
+ end else
+ (* bytecode (we shunt ocamlmktop script which fails on win32) *)
+ let ocamlmktoplib = " toplevellib.cma" in
+ let ocamlcexec = Filename.concat Coq_config.camldir "ocamlc" in
+- let ocamlccustom = ocamlcexec^" -custom -linkall" in
++ let ocamlccustom = ocamlcexec^" -custom -linkall -rectypes" in
+ (if !top then ocamlccustom^ocamlmktoplib else ocamlccustom)
+ in
+ (* files to link *)
+diff -urNad coq-8.1.pl1+dfsg~/tools/coq_makefile.ml4 coq-8.1.pl1+dfsg/tools/coq_makefile.ml4
+--- coq-8.1.pl1+dfsg~/tools/coq_makefile.ml4 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/tools/coq_makefile.ml4 2007-08-24 10:56:52.000000000 +0000
+@@ -175,7 +175,7 @@
+ | _ :: r -> var_aux r
+ in
+ section "Variables definitions.";
+- print "CAMLP4LIB=`camlp4 -where`\n";
++ print "CAMLP4LIB=`camlp5 -where`\n";
+ (* print "MAKE=make \"COQBIN=$(COQBIN)\" \"OPT=$(OPT)\"\n"; *)
+ print "COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
+ -I $(COQTOP)/library -I $(COQTOP)/parsing \\
+@@ -204,8 +204,8 @@
+ print "CAMLOPTLINK=ocamlopt\n";
+ print "COQDEP=$(COQBIN)coqdep -c\n";
+ print "GRAMMARS=grammar.cma\n";
+- print "CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo\n";
+- print "PP=-pp \"camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n";
++ print "CAMLP4EXTEND=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
++ print "PP=-pp \"camlp5o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n";
+ var_aux l;
+ print "\n"
+
+diff -urNad coq-8.1.pl1+dfsg~/toplevel/metasyntax.ml coq-8.1.pl1+dfsg/toplevel/metasyntax.ml
+--- coq-8.1.pl1+dfsg~/toplevel/metasyntax.ml 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/toplevel/metasyntax.ml 2007-08-24 10:56:52.000000000 +0000
+@@ -28,7 +28,7 @@
+ (**********************************************************************)
+ (* Tokens *)
+
+-let cache_token (_,s) = Pcoq.lexer.Token.using ("", s)
++let cache_token (_,s) = Pcoq.lexer.Token.tok_using ("", s)
+
+ let (inToken, outToken) =
+ declare_object {(default_object "TOKEN") with
+diff -urNad coq-8.1.pl1+dfsg~/toplevel/mltop.ml4 coq-8.1.pl1+dfsg/toplevel/mltop.ml4
+--- coq-8.1.pl1+dfsg~/toplevel/mltop.ml4 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/toplevel/mltop.ml4 2007-08-24 10:56:52.000000000 +0000
+@@ -98,7 +98,7 @@
+ str s; str" to Coq code." >])
+ (* TO DO: .cma loading without toplevel *)
+ | WithoutTop ->
+- ifdef Byte then
++ IFDEF Byte THEN
+ let _,gname = where_in_path !coq_mlpath_copy s in
+ try
+ Dynlink.loadfile gname;
+@@ -108,7 +108,7 @@
+ [Filename.dirname gname]
+ with | Dynlink.Error a ->
+ errorlabstrm "Mltop.load_object" [< str (Dynlink.error_message a) >]
+- else ()
++ ELSE () END
+ | Native ->
+ errorlabstrm "Mltop.no_load_object"
+ [< str"Loading of ML object file forbidden in a native Coq" >]
+diff -urNad coq-8.1.pl1+dfsg~/toplevel/toplevel.ml coq-8.1.pl1+dfsg/toplevel/toplevel.ml
+--- coq-8.1.pl1+dfsg~/toplevel/toplevel.ml 2007-08-24 10:56:51.000000000 +0000
++++ coq-8.1.pl1+dfsg/toplevel/toplevel.ml 2007-08-24 10:56:52.000000000 +0000
+@@ -139,16 +139,16 @@
+
+ (* Functions to report located errors in a file. *)
+
+-let print_location_in_file s inlibrary fname (bp,ep) =
++let print_location_in_file s inlibrary fname loc =
+ let errstrm = (str"Error while reading " ++ str s ++ str" :" ++ fnl ()) in
+- if (bp,ep) = dummy_loc then
++ if loc = dummy_loc then
+ (errstrm ++ str", unknown location." ++ fnl ())
+ else
+ if inlibrary then
+ (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++
+- str" characters " ++ Cerrors.print_loc (bp,ep) ++ fnl ())
++ str" characters " ++ Cerrors.print_loc loc ++ fnl ())
+ else
+- let (bp,ep) = unloc (bp,ep) in
++ let (bp,ep) = unloc loc in
+ let ic = open_in fname in
+ let rec line_of_pos lin bol cnt =
+ if cnt < bp then
+@@ -172,15 +172,16 @@
+ str(String.sub ib.str (bp-ib.start) (ep-bp)) ++ fnl ())
+ | None -> (mt ())
+
+-let valid_loc dloc (b,e) =
+- (b,e) <> dummy_loc
++let valid_loc dloc loc =
++ let b, e = unloc loc in
++ loc <> dummy_loc
+ & match dloc with
+- | Some (bd,ed) -> bd<=b & e<=ed
++ | Some dloc -> let bd,ed = unloc dloc in bd<=b & e<=ed
+ | _ -> true
+
+-let valid_buffer_loc ib dloc (b,e) =
+- valid_loc dloc (b,e) &
+- let (b,e) = unloc (b,e) in b-ib.start >= 0 & e-ib.start < ib.len & b<=e
++let valid_buffer_loc ib dloc loc =
++ valid_loc dloc loc &
++ let (b,e) = unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e
+
+ (*s The Coq prompt is the name of the focused proof, if any, and "Coq"
+ otherwise. We trap all exceptions to prevent the error message printing
diff --git a/debian/patches/cmxa-install.dpatch b/debian/patches/cmxa-install.dpatch
new file mode 100755
index 00000000..7e8d2ffb
--- /dev/null
+++ b/debian/patches/cmxa-install.dpatch
@@ -0,0 +1,23 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## cmxa-install.dpatch by Samuel Mimram <smimram@debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: .cmxa are not generated on non-native archs, so don't install them.
+
+@DPATCH@
+diff -urNad coq-8.1+dfsg~/Makefile coq-8.1+dfsg/Makefile
+--- coq-8.1+dfsg~/Makefile 2007-02-18 13:25:29.000000000 +0100
++++ coq-8.1+dfsg/Makefile 2007-02-18 13:27:28.000000000 +0100
+@@ -1272,7 +1272,11 @@
+ parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \
+ parsing/highparsing.cma tactics/hightactics.cma contrib/contrib.cma
+
+-OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa)
++ifeq ($(BEST),opt)
++ OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa)
++else
++ OBJECTCMXA=
++endif
+
+ install-library:
+ $(MKDIR) $(FULLCOQLIB)
diff --git a/debian/patches/configure.dpatch b/debian/patches/configure.dpatch
new file mode 100755
index 00000000..db3ef2a5
--- /dev/null
+++ b/debian/patches/configure.dpatch
@@ -0,0 +1,19 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## configure.dpatch by Pierre Letouzey <pierre.letouzey@pps.jussieu.fr>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Correctly detect whether ocamlopt is present or not.
+
+@DPATCH@
+diff -urNad coq-8.1+dfsg~/configure coq-8.1+dfsg/configure
+--- coq-8.1+dfsg~/configure 2007-02-10 08:32:28.000000000 +0000
++++ coq-8.1+dfsg/configure 2007-02-15 12:58:56.000000000 +0000
+@@ -340,7 +340,7 @@
+ # do we have a native compiler: test of ocamlopt and its version
+
+ if [ "$best_compiler" = "opt" ] ; then
+- if test -e `which "$nativecamlc"` ; then
++ if test -e "`which $nativecamlc`" ; then
+ CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
+ if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then
+ echo "native and bytecode compilers do not have the same version!"; fi
diff --git a/debian/patches/coqdoc_stdlib.dpatch b/debian/patches/coqdoc_stdlib.dpatch
new file mode 100755
index 00000000..fb618f56
--- /dev/null
+++ b/debian/patches/coqdoc_stdlib.dpatch
@@ -0,0 +1,19 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## coqdoc_stdlib.dpatch by Samuel Mimram <smimram@debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Add an option to coqdoc to be able to use a custom stdlib path in order
+## DP: to be able to build the documentation before coqdoc is installed.
+
+@DPATCH@
+diff -urNad coq-8.0pl3+8.1beta~/doc/Makefile coq-8.0pl3+8.1beta/doc/Makefile
+--- coq-8.0pl3+8.1beta~/doc/Makefile 2006-06-16 13:02:33.000000000 +0000
++++ coq-8.0pl3+8.1beta/doc/Makefile 2006-06-16 13:19:11.000000000 +0000
+@@ -216,6 +216,7 @@
+ mkdir stdlib/html
+ (cd stdlib/html;\
+ $(COQDOC) -q --multi-index --html --glob-from $(GLOBDUMP)\
++ --coqlib_path $(COQTOP) \
+ -R $(COQTOP)/theories Coq $(COQTOP)/theories/*/*.v)
+ mv stdlib/html/index.html stdlib/index-body.html
+
diff --git a/debian/patches/makefile.dpatch b/debian/patches/makefile.dpatch
new file mode 100755
index 00000000..b656a9bb
--- /dev/null
+++ b/debian/patches/makefile.dpatch
@@ -0,0 +1,20 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## makefile.dpatch by Samuel Mimram <smimram@debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Do not use ocamlopt to test grammar.cma, we don't want to use ocamlopt
+## DP: when compiling on non-native archs.
+
+@DPATCH@
+diff -urNad coq-8.0pl3+8.1alpha~/Makefile coq-8.0pl3+8.1alpha/Makefile
+--- coq-8.0pl3+8.1alpha~/Makefile 2006-04-07 15:08:12.000000000 +0000
++++ coq-8.0pl3+8.1alpha/Makefile 2006-04-30 11:41:09.000000000 +0000
+@@ -1401,7 +1401,7 @@
+ parsing/grammar.cma: $(GRAMMARCMO)
+ $(SHOW)'Testing $@'
+ @touch test.ml4
+- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
++ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
+ @rm -f test-grammar test.*
+ $(SHOW)'OCAMLC -a $@'
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@
diff --git a/debian/patches/no-complexity-test.dpatch b/debian/patches/no-complexity-test.dpatch
new file mode 100644
index 00000000..bf89f1f7
--- /dev/null
+++ b/debian/patches/no-complexity-test.dpatch
@@ -0,0 +1,21 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## no-complexity-test.dpatch by Julien Cristau <julien.cristau@ens-lyon.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Don't run complexity tests, they are far too fragile.
+
+@DPATCH@
+diff -urNad coq-8.1gamma~/test-suite/check coq-8.1gamma/test-suite/check
+--- coq-8.1gamma~/test-suite/check 2006-11-03 14:07:27.000000000 +0100
++++ coq-8.1gamma/test-suite/check 2006-11-23 15:19:49.000000000 +0100
+@@ -145,8 +145,8 @@
+ test_parser parser
+ echo "Interactive tests"
+ test_interactive interactive
+-echo "Complexity tests"
+-test_complexity complexity
++echo "Skipping complexity tests"
++#test_complexity complexity
+ echo "Module tests"
+ $coqtop -compile modules/Nat
+ $coqtop -compile modules/plik
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-15 17:49:24 +0000