diff options
-rw-r--r-- | config/Makefile.template | 2 | ||||
-rw-r--r-- | parsing/ppconstr.ml | 8 | ||||
-rw-r--r-- | parsing/ppvernac.ml | 4 | ||||
-rw-r--r-- | parsing/q_util.ml4 | 6 | ||||
-rw-r--r-- | parsing/tacextend.ml4 | 2 | ||||
-rw-r--r-- | parsing/vernacextend.ml4 | 2 | ||||
-rw-r--r-- | toplevel/toplevel.ml | 21 |
7 files changed, 23 insertions, 22 deletions
diff --git a/config/Makefile.template b/config/Makefile.template index d4fa11783..6161089ae 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -65,7 +65,7 @@ CAMLOPTLINK="NATIVECAMLC" CAMLMKTOP="CAMLMKTOPEXEC" # Caml flags -CAMLFLAGS=CAMLANNOTATEFLAG +CAMLFLAGS=-rectypes CAMLANNOTATEFLAG # Compilation debug flag CAMLDEBUG=COQDEBUGFLAG diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 65439dd26..9b257014e 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -95,9 +95,9 @@ let pr_patnotation = pr_notation_gen decode_patlist_value 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 @@ let pr_opt_type_spc pr = function | 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 --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 668cfe6f3..d44e225b5 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -28,7 +28,7 @@ open Tacinterp 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 string_of_fqid fqid = 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 --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index 7c684cdc1..513d345b5 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -39,18 +39,18 @@ let mlexpr_of_list f l = 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 --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 476732a3f..6e8425d98 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -10,12 +10,12 @@ (* $Id$ *) +open Util open Genarg open Q_util open Q_coqast open Argextend -let join_loc (deb1,_) (_,fin2) = (deb1,fin2) let loc = Util.dummy_loc let default_loc = <:expr< Util.dummy_loc >> diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 3c8526c08..0b3dd75ad 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -10,12 +10,12 @@ (* $Id$ *) +open Util open Genarg open Q_util open Q_coqast open Argextend -let join_loc (deb1,_) (_,fin2) = (deb1,fin2) let loc = Util.dummy_loc let default_loc = <:expr< Util.dummy_loc >> diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 7f21de041..fbdc96d6e 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -139,16 +139,16 @@ let print_highlight_location ib loc = (* 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 @@ let print_command_location ib dloc = 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 = + loc <> dummy_loc & match dloc with - | Some (bd,ed) -> bd<=b & e<=ed + | Some dloc -> + let (bd,ed) = unloc dloc in let (b,e) = unloc loc 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 |