6 files changed, 41 insertions, 7 deletions
diff --git a/lib/cArray.ml b/lib/cArray.ml
index d08f24d490..013585735c 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -334,7 +334,7 @@ let smartmap f (ar : 'a array) =
     Array.unsafe_set ans !i v;
     incr i;
     while !i < len do
-      let v = Array.unsafe_get ar !i in
+      let v = Array.unsafe_get ans !i in
       let v' = f v in
       if v != v' then Array.unsafe_set ans !i v';
       incr i
@@ -527,7 +527,7 @@ struct
       Array.unsafe_set ans !i v;
       incr i;
       while !i < len do
-        let v = Array.unsafe_get ar !i in
+        let v = Array.unsafe_get ans !i in
         let v' = f arg v in
         if v != v' then Array.unsafe_set ans !i v';
         incr i
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index 13de731f54..970666638c 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -206,7 +206,7 @@ let rec find_project_file ~from ~projfile_name =
   if Sys.file_exists fname then Some fname
   else
     let newdir = Filename.dirname from in
-    if newdir = "" || newdir = "/" then None
+    if newdir = from then None
     else find_project_file ~from:newdir ~projfile_name
 ;;
 
diff --git a/lib/loc.ml b/lib/loc.ml
index 9f036d90f9..4a935a9d9c 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -8,8 +8,12 @@
 
 (* Locations management *)
 
+type source =
+  | InFile of string
+  | ToplevelInput
+
 type t = {
-  fname : string; (** filename *)
+  fname : source; (** filename or toplevel input *)
   line_nb : int; (** start line number *)
   bol_pos : int; (** position of the beginning of start line *)
   line_nb_last : int; (** end line number *)
@@ -23,10 +27,15 @@ let create fname line_nb bol_pos bp ep = {
   line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; }
 
 let make_loc (bp, ep) = {
-  fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
+  fname = ToplevelInput; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
   bp = bp; ep = ep; }
 
+let mergeable loc1 loc2 =
+  loc1.fname = loc2.fname
+
 let merge loc1 loc2 =
+  if not (mergeable loc1 loc2) then
+    failwith "Trying to merge unmergeable locations.";
   if loc1.bp < loc2.bp then
     if loc1.ep < loc2.ep then {
       fname = loc1.fname;
@@ -53,6 +62,8 @@ let merge_opt l1 l2 = match l1, l2 with
 
 let unloc loc = (loc.bp, loc.ep)
 
+let shift_loc kb kp loc = { loc with bp = loc.bp + kb ; ep = loc.ep + kp }
+
 (** Located type *)
 type 'a located = t option * 'a
 
diff --git a/lib/loc.mli b/lib/loc.mli
index 1fbaae8368..fde490cc8a 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -8,8 +8,12 @@
 
 (** {5 Basic types} *)
 
+type source =
+  | InFile of string
+  | ToplevelInput
+
 type t = {
-  fname : string; (** filename *)
+  fname : source; (** filename or toplevel input *)
   line_nb : int; (** start line number *)
   bol_pos : int; (** position of the beginning of start line *)
   line_nb_last : int; (** end line number *)
@@ -22,7 +26,7 @@ type t = {
 
 (** This is inherited from CAMPL4/5. *)
 
-val create : string -> int -> int -> int -> int -> t
+val create : source -> int -> int -> int -> int -> t
 (** Create a location from a filename, a line number, a position of the
     beginning of the line, a start and end position *)
 
@@ -36,6 +40,11 @@ val merge : t -> t -> t
 val merge_opt : t option -> t option -> t option
 (** Merge locations, usually generating the largest possible span *)
 
+val shift_loc : int -> int -> t -> t
+(** [shift_loc loc n p] shifts the beginning of location by [n] and
+    the end by [p]; it is assumed that the shifts do not change the
+    lines at which the location starts and ends *)
+
 (** {5 Located exceptions} *)
 
 val add_loc : Exninfo.info -> t -> Exninfo.info
diff --git a/lib/util.ml b/lib/util.ml
index 36282b2dac..6de012da0e 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -171,3 +171,12 @@ let open_utf8_file_in fname =
   let s = Bytes.make 3 ' ' in
   if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0;
   in_chan
+
+(** A trick which can typically be used to store on the fly the
+   computation of values in the "when" clause of a "match" then
+   retrieve the evaluated result in the r.h.s of the clause *)
+
+let set_temporary_memory () =
+  let a = ref None in
+  (fun x -> assert (!a = None); a := Some x; x),
+  (fun () -> match !a with Some x -> x | None -> assert false)
diff --git a/lib/util.mli b/lib/util.mli
index d910e7e28e..c54f5825cd 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -137,3 +137,8 @@ val sym : ('a, 'b) eq -> ('b, 'a) eq
 
 val open_utf8_file_in : string -> in_channel
 (** Open an utf-8 encoded file and skip the byte-order mark if any. *)
+
+val set_temporary_memory : unit -> ('a -> 'a) * (unit -> 'a)
+(** A trick which can typically be used to store on the fly the
+   computation of values in the "when" clause of a "match" then
+   retrieve the evaluated result in the r.h.s of the clause *)