summaryrefslogtreecommitdiff
path: root/debian/patches/camlp5.dpatch
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-08-24 08:02:00 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-08-24 08:02:00 +0000
commit9b1df26176ec4805885b9a653b38d7e84a2c9d71 (patch)
tree7d3a123630c21791b8446be65b536115088ea08b /debian/patches/camlp5.dpatch
parent87eadccc94d459a90938ce6b15fba40ac000d8d7 (diff)
Updated camlp5 patch.
Diffstat (limited to 'debian/patches/camlp5.dpatch')
-rwxr-xr-xdebian/patches/camlp5.dpatch133
1 files changed, 88 insertions, 45 deletions
diff --git a/debian/patches/camlp5.dpatch b/debian/patches/camlp5.dpatch
index 9de2b6a7..a8a9a993 100755
--- a/debian/patches/camlp5.dpatch
+++ b/debian/patches/camlp5.dpatch
@@ -2,12 +2,12 @@
## camlp5.dpatch by Samuel Mimram <smimram@debian.org>
##
## All lines beginning with `## DP:' are a description of the patch.
-## DP: No description.
+## 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-22 16:33:31.000000000 +0000
-+++ coq-8.1.pl1+dfsg/Makefile 2007-08-22 16:36:36.000000000 +0000
+--- coq-8.1.pl1+dfsg~/Makefile 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/Makefile 2007-08-23 23:19:38.000000000 +0000
@@ -1504,11 +1504,11 @@
# BEFOREDEPEND+= parsing/pcoq.ml parsing/extend.ml
@@ -60,8 +60,8 @@ diff -urNad coq-8.1.pl1+dfsg~/Makefile coq-8.1.pl1+dfsg/Makefile
#.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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/Makefile.dep 2007-08-22 16:36:36.000000000 +0000
+--- coq-8.1.pl1+dfsg~/Makefile.dep 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/Makefile.dep 2007-08-23 23:19:38.000000000 +0000
@@ -12,4 +12,4 @@
include .depend.camlp4
@@ -69,8 +69,8 @@ diff -urNad coq-8.1.pl1+dfsg~/Makefile.dep coq-8.1.pl1+dfsg/Makefile.dep
- $(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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/config/Makefile.template 2007-08-22 16:36:36.000000000 +0000
+--- coq-8.1.pl1+dfsg~/config/Makefile.template 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/config/Makefile.template 2007-08-23 23:21:52.000000000 +0000
@@ -62,7 +62,7 @@
CAMLMKTOP="CAMLMKTOPEXEC"
@@ -80,9 +80,20 @@ diff -urNad coq-8.1.pl1+dfsg~/config/Makefile.template coq-8.1.pl1+dfsg/config/M
# 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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/configure 2007-08-22 16:36:36.000000000 +0000
+--- coq-8.1.pl1+dfsg~/configure 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/configure 2007-08-23 23:19:38.000000000 +0000
@@ -78,7 +78,7 @@
ocamllexexec=ocamllex
ocamlyaccexec=ocamlyacc
@@ -143,9 +154,21 @@ diff -urNad coq-8.1.pl1+dfsg~/configure coq-8.1.pl1+dfsg/configure
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 2006-10-13 20:29:04.000000000 +0000
++++ coq-8.1.pl1+dfsg/dev/ocamldebug-coq.template 2007-08-23 23:25:35.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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/lib/compat.ml4 2007-08-22 16:36:36.000000000 +0000
+--- coq-8.1.pl1+dfsg~/lib/compat.ml4 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/lib/compat.ml4 2007-08-23 23:19:38.000000000 +0000
@@ -11,6 +11,7 @@
(* IFDEF not available in 3.06; use ifdef instead *)
@@ -169,8 +192,8 @@ diff -urNad coq-8.1.pl1+dfsg~/lib/compat.ml4 coq-8.1.pl1+dfsg/lib/compat.ml4
+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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/lib/util.ml 2007-08-22 16:36:36.000000000 +0000
+--- coq-8.1.pl1+dfsg~/lib/util.ml 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/lib/util.ml 2007-08-23 23:19:38.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 =
@@ -181,8 +204,8 @@ diff -urNad coq-8.1.pl1+dfsg~/lib/util.ml coq-8.1.pl1+dfsg/lib/util.ml
(* 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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/parsing/argextend.ml4 2007-08-22 16:36:45.000000000 +0000
+--- coq-8.1.pl1+dfsg~/parsing/argextend.ml4 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/argextend.ml4 2007-08-23 23:19:38.000000000 +0000
@@ -12,7 +12,7 @@
open Q_util
open Q_coqast
@@ -202,8 +225,8 @@ diff -urNad coq-8.1.pl1+dfsg~/parsing/argextend.ml4 coq-8.1.pl1+dfsg/parsing/arg
] ]
;
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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/parsing/egrammar.mli 2007-08-22 16:36:45.000000000 +0000
+--- coq-8.1.pl1+dfsg~/parsing/egrammar.mli 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/egrammar.mli 2007-08-23 23:19:38.000000000 +0000
@@ -45,7 +45,7 @@
type grammar_tactic_production =
| TacTerm of string
@@ -223,8 +246,8 @@ diff -urNad coq-8.1.pl1+dfsg~/parsing/egrammar.mli coq-8.1.pl1+dfsg/parsing/egra
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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/parsing/pcoq.ml4 2007-08-22 16:36:45.000000000 +0000
+--- coq-8.1.pl1+dfsg~/parsing/pcoq.ml4 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/pcoq.ml4 2007-08-23 23:19:38.000000000 +0000
@@ -30,20 +30,23 @@
lexer. B.B. *)
@@ -265,8 +288,8 @@ diff -urNad coq-8.1.pl1+dfsg~/parsing/pcoq.ml4 coq-8.1.pl1+dfsg/parsing/pcoq.ml4
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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/parsing/pcoq.mli 2007-08-22 16:36:36.000000000 +0000
+--- coq-8.1.pl1+dfsg~/parsing/pcoq.mli 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/pcoq.mli 2007-08-23 23:19:38.000000000 +0000
@@ -20,9 +20,9 @@
(* The lexer and parser of Coq. *)
@@ -298,8 +321,8 @@ diff -urNad coq-8.1.pl1+dfsg~/parsing/pcoq.mli coq-8.1.pl1+dfsg/parsing/pcoq.mli
(* 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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/parsing/ppconstr.ml 2007-08-22 16:36:45.000000000 +0000
+--- coq-8.1.pl1+dfsg~/parsing/ppconstr.ml 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/ppconstr.ml 2007-08-23 23:19:38.000000000 +0000
@@ -95,9 +95,9 @@
let pr_delimiters key strm =
strm ++ str ("%"^key)
@@ -323,8 +346,8 @@ diff -urNad coq-8.1.pl1+dfsg~/parsing/ppconstr.ml coq-8.1.pl1+dfsg/parsing/ppcon
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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/parsing/ppvernac.ml 2007-08-22 16:36:45.000000000 +0000
+--- coq-8.1.pl1+dfsg~/parsing/ppvernac.ml 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/ppvernac.ml 2007-08-23 23:19:38.000000000 +0000
@@ -28,7 +28,7 @@
let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
@@ -344,8 +367,8 @@ diff -urNad coq-8.1.pl1+dfsg~/parsing/ppvernac.ml coq-8.1.pl1+dfsg/parsing/ppver
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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/parsing/q_coqast.ml4 2007-08-22 16:36:45.000000000 +0000
+--- coq-8.1.pl1+dfsg~/parsing/q_coqast.ml4 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/q_coqast.ml4 2007-08-23 23:19:38.000000000 +0000
@@ -22,10 +22,8 @@
let anti loc x =
let e =
@@ -360,8 +383,8 @@ diff -urNad coq-8.1.pl1+dfsg~/parsing/q_coqast.ml4 coq-8.1.pl1+dfsg/parsing/q_co
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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/parsing/q_util.ml4 2007-08-22 16:36:45.000000000 +0000
+--- coq-8.1.pl1+dfsg~/parsing/q_util.ml4 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/q_util.ml4 2007-08-23 23:19:38.000000000 +0000
@@ -37,18 +37,18 @@
List.fold_right
(fun e1 e2 ->
@@ -385,8 +408,8 @@ diff -urNad coq-8.1.pl1+dfsg~/parsing/q_util.ml4 coq-8.1.pl1+dfsg/parsing/q_util
(* 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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/parsing/tacextend.ml4 2007-08-22 16:36:45.000000000 +0000
+--- coq-8.1.pl1+dfsg~/parsing/tacextend.ml4 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/tacextend.ml4 2007-08-23 23:19:38.000000000 +0000
@@ -13,7 +13,7 @@
open Q_coqast
open Argextend
@@ -397,8 +420,8 @@ diff -urNad coq-8.1.pl1+dfsg~/parsing/tacextend.ml4 coq-8.1.pl1+dfsg/parsing/tac
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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/parsing/vernacextend.ml4 2007-08-22 16:36:45.000000000 +0000
+--- coq-8.1.pl1+dfsg~/parsing/vernacextend.ml4 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/vernacextend.ml4 2007-08-23 23:19:38.000000000 +0000
@@ -13,7 +13,7 @@
open Q_coqast
open Argextend
@@ -409,8 +432,17 @@ diff -urNad coq-8.1.pl1+dfsg~/parsing/vernacextend.ml4 coq-8.1.pl1+dfsg/parsing/
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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/scripts/coqmktop.ml 2007-08-22 16:36:45.000000000 +0000
+--- coq-8.1.pl1+dfsg~/scripts/coqmktop.ml 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/scripts/coqmktop.ml 2007-08-23 23:26:36.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"; "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 !";
@@ -427,20 +459,31 @@ diff -urNad coq-8.1.pl1+dfsg~/scripts/coqmktop.ml coq-8.1.pl1+dfsg/scripts/coqmk
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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/tools/coq_makefile.ml4 2007-08-22 16:36:36.000000000 +0000
-@@ -204,7 +204,7 @@
+--- coq-8.1.pl1+dfsg~/tools/coq_makefile.ml4 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/tools/coq_makefile.ml4 2007-08-23 23:20:24.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 \"camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/toplevel/metasyntax.ml 2007-08-22 16:36:45.000000000 +0000
+--- coq-8.1.pl1+dfsg~/toplevel/metasyntax.ml 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/toplevel/metasyntax.ml 2007-08-23 23:19:38.000000000 +0000
@@ -28,7 +28,7 @@
(**********************************************************************)
(* Tokens *)
@@ -451,8 +494,8 @@ diff -urNad coq-8.1.pl1+dfsg~/toplevel/metasyntax.ml coq-8.1.pl1+dfsg/toplevel/m
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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/toplevel/mltop.ml4 2007-08-22 16:36:45.000000000 +0000
+--- coq-8.1.pl1+dfsg~/toplevel/mltop.ml4 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/toplevel/mltop.ml4 2007-08-23 23:19:38.000000000 +0000
@@ -98,7 +98,7 @@
str s; str" to Coq code." >])
(* TO DO: .cma loading without toplevel *)
@@ -472,8 +515,8 @@ diff -urNad coq-8.1.pl1+dfsg~/toplevel/mltop.ml4 coq-8.1.pl1+dfsg/toplevel/mltop
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-22 16:33:10.000000000 +0000
-+++ coq-8.1.pl1+dfsg/toplevel/toplevel.ml 2007-08-22 16:36:45.000000000 +0000
+--- coq-8.1.pl1+dfsg~/toplevel/toplevel.ml 2007-08-23 23:19:37.000000000 +0000
++++ coq-8.1.pl1+dfsg/toplevel/toplevel.ml 2007-08-23 23:19:38.000000000 +0000
@@ -139,16 +139,16 @@
(* Functions to report located errors in a file. *)