Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

8 files changed, 58 insertions, 134 deletions

diff --git a/library/assumptions.ml b/library/assumptions.ml
index adc7f8ed..d2f8ad53 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -54,6 +54,16 @@ module ContextObjectMap = Map.Make (OrderedContextObject)
 
 let modcache = ref (MPmap.empty : structure_body MPmap.t)
 
+let rec search_mod_label lab = function
+  | [] -> raise Not_found
+  | (l,SFBmodule mb) :: _ when l = lab -> mb
+  | _ :: fields -> search_mod_label lab fields
+
+let rec search_cst_label lab = function
+  | [] -> raise Not_found
+  | (l,SFBconst cb) :: _ when l = lab -> cb
+  | _ :: fields -> search_cst_label lab fields
+
 let rec lookup_module_in_impl mp =
   try Global.lookup_module mp
   with Not_found ->
@@ -64,9 +74,7 @@ let rec lookup_module_in_impl mp =
 	raise Not_found (* should have been found by [lookup_module] *)
       | MPdot (mp',lab') ->
 	let fields = memoize_fields_of_mp mp' in
-	match List.assoc lab' fields with
-	  | SFBmodule mb -> mb
-	  | _ -> assert false (* same label for a non-module ?! *)
+	search_mod_label lab' fields
 
 and memoize_fields_of_mp mp =
   try MPmap.find mp !modcache
@@ -126,9 +134,7 @@ let lookup_constant_in_impl cst fallback =
     let fields = memoize_fields_of_mp mp in
     (* A module found this way is necessarily closed, in particular
        our constant cannot be in an opened section : *)
-    match List.assoc lab fields with
-      | SFBconst cb -> cb
-      | _ -> assert false (* label not pointing to a constant ?! *)
+    search_cst_label lab fields
   with Not_found ->
     (* Either:
        - The module part of the constant isn't registered yet :
diff --git a/library/declare.ml b/library/declare.ml
index 28858085..066c97a4 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -116,7 +116,7 @@ let open_constant i ((sp,kn),_) =
     Nametab.push (Nametab.Exactly i) sp (ConstRef con)
 
 let exists_name id =
-  variable_exists id or Global.exists_label (label_of_id id)
+  variable_exists id or Global.exists_objlabel (label_of_id id)
 
 let check_exists sp =
   let id = basename sp in
diff --git a/library/global.ml b/library/global.ml
index ab70bb7c..a0871f0c 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -133,7 +133,7 @@ let mind_of_delta_kn kn =
     Mod_subst.mind_of_delta resolver_param
       (Mod_subst.mind_of_delta_kn resolver kn)
 
-let exists_label id = exists_label id !global_env
+let exists_objlabel id = exists_objlabel id !global_env
 
 let start_library dir =
   let mp,newenv = start_library dir !global_env in
diff --git a/library/global.mli b/library/global.mli
index 1a0fabdc..77fd465c 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -87,7 +87,7 @@ val lookup_module    : module_path -> module_body
 val lookup_modtype   : module_path -> module_type_body
 val constant_of_delta_kn : kernel_name -> constant
 val mind_of_delta_kn : kernel_name -> mutual_inductive
-val exists_label     : label -> bool
+val exists_objlabel  : label -> bool
 
 (** Compiled modules *)
 val start_library : dir_path -> module_path
diff --git a/library/goptions.ml b/library/goptions.ml
index 90c8728c..5af18689 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -247,6 +247,7 @@ let declare_option cast uncast
       declare_object {(default_object ("G  "^nickname key)) with
 		       cache_function = (fun (_,v) -> write v);
 		       classify_function = (fun v -> Substitute v);
+		       subst_function = (fun (_,v) -> v);
 		       discharge_function = (fun (_,v) -> Some v);
 		       load_function = (fun _ (_,v) -> write v)}
     in
diff --git a/library/impargs.ml b/library/impargs.ml
index ef7f5921..73699a90 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -207,11 +207,10 @@ let rec is_rigid_head t = match kind_of_term t with
 
 (* calcule la liste des arguments implicites *)
 
-let find_displayed_name_in all avoid na b =
-  if all then
-    compute_and_force_displayed_name_in (RenamingElsewhereFor b) avoid na b
-  else
-    compute_displayed_name_in (RenamingElsewhereFor b) avoid na b
+let find_displayed_name_in all avoid na (_,b as envnames_b) =
+  let flag = RenamingElsewhereFor envnames_b in
+  if all then compute_and_force_displayed_name_in flag avoid na b
+  else compute_displayed_name_in flag avoid na b
 
 let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   let rigid = ref true in
@@ -219,7 +218,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
     let t = whd_betadeltaiota env t in
     match kind_of_term t with
       | Prod (na,a,b) ->
-	  let na',avoid' = find_displayed_name_in all avoid na b in
+	  let na',avoid' = find_displayed_name_in all avoid na (names,b) in
 	  add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
             (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
       | _ ->
@@ -232,7 +231,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   in
   match kind_of_term (whd_betadeltaiota env t) with
     | Prod (na,a,b) ->
-	let na',avoid = find_displayed_name_in all [] na b in
+	let na',avoid = find_displayed_name_in all [] na ([],b) in
 	let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
 	!rigid, Array.to_list v
     | _ -> true, []
diff --git a/library/lib.ml b/library/lib.ml
index 7554fd0b..bb3b5716 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -572,72 +572,16 @@ let reset_to_gen test =
 
 let reset_to sp = reset_to_gen (fun x -> fst x = sp)
 
-(* LEM: TODO
- * We will need to muck with frozen states in after, too!
- * Not only FrozenState, but also those embedded in Opened(Section|Module)
- *)
-let delete_gen test =
-  let (after,equal,before) = split_lib_gen test in
-  let rec chop_at_dot = function
-    | [] as l -> l
-    | (_, Leaf o)::t when object_tag o = "DOT" -> t
-    | _::t -> chop_at_dot t
-  and chop_before_dot = function
-    | [] as l -> l
-    | (_, Leaf o)::t as l when object_tag o = "DOT" -> l
-    | _::t -> chop_before_dot t
- in
-  set_lib_stk (List.rev_append (chop_at_dot after) (chop_before_dot before))
-
-let delete sp = delete_gen (fun x -> fst x = sp)
-
-let reset_name (loc,id) =
-  let (sp,_) =
-    try
-      find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi)
-    with Not_found ->
-      user_err_loc (loc,"reset_name",pr_id id ++ str ": no such entry")
-  in
-  reset_to sp
-
-let remove_name (loc,id) =
-  let (sp,_) =
-    try
-      find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi)
-    with Not_found ->
-      user_err_loc (loc,"remove_name",pr_id id ++ str ": no such entry")
-  in
-    delete sp
+let first_command_label = 1
 
-let is_mod_node = function
-  | OpenedModule _ | OpenedSection _
-  | ClosedModule _ | ClosedSection _  -> true
-  | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE"
-	|| t = "MODULE ALIAS"
-  | _ -> false
-
-(* Reset on a module or section name in order to bypass constants with
-   the same name *)
-
-let reset_mod (loc,id) =
-  let (_,before) =
-    try
-      find_split_p (fun (sp,node) ->
-                    let (_,spi) = repr_path (fst sp) in id = spi
-                    && is_mod_node node)
-    with Not_found ->
-      user_err_loc (loc,"reset_mod",pr_id id ++ str ": no such entry")
-  in
-  set_lib_stk before
-
-let mark_end_of_command, current_command_label, set_command_label =
-  let n = ref 0 in
+let mark_end_of_command, current_command_label, reset_command_label =
+  let n = ref (first_command_label-1) in
   (fun () ->
     match !lib_stk with
         (_,Leaf o)::_ when object_tag o = "DOT" -> ()
       | _ -> incr n;add_anonymous_leaf (inLabel !n)),
   (fun () -> !n),
-  (fun x -> n:=x)
+  (fun x -> n:=x;add_anonymous_leaf (inLabel x))
 
 let is_label_n n x =
   match x with
@@ -650,21 +594,21 @@ let is_label_n n x =
 let reset_label n =
   if n >= current_command_label () then
     error "Cannot backtrack to the current label or a future one";
-  let res = reset_to_gen (is_label_n n) in
+  reset_to_gen (is_label_n n);
   (* forget state numbers after n only if reset succeeded *)
-  set_command_label (n-1);
-  res
+  reset_command_label n
 
-let rec back_stk n stk =
-  match stk with
-      (sp,Leaf o)::tail when object_tag o = "DOT" ->
-        if n=0 then sp else back_stk (n-1) tail
-    | _::tail -> back_stk n tail
-    | [] -> error "Reached begin of command history"
+(** Search the last label registered before defining [id] *)
 
-let back n =
-  reset_to (back_stk n !lib_stk);
-  set_command_label (current_command_label () - n - 1)
+let label_before_name (loc,id) =
+  let found = ref false in
+  let search = function
+    | (_,Leaf o) when !found && object_tag o = "DOT" -> true
+    | (sp,_) -> (if id = snd (repr_path (fst sp)) then found := true); false
+  in
+  match find_entry_p search with
+    | (_,Leaf o) -> outLabel o
+    | _ -> raise Not_found
 
 (* State and initialization. *)
 
@@ -684,29 +628,6 @@ let init () =
   path_prefix := initial_prefix;
   init_summaries()
 
-(* Initial state. *)
-
-let initial_state = ref None
-
-let declare_initial_state () =
-  let name = add_anonymous_entry (FrozenState (freeze_summaries())) in
-  initial_state := Some name
-
-let reset_initial () =
-  match !initial_state with
-    | None ->
-        error "Resetting to the initial state is possible only interactively"
-    | Some sp ->
-  	begin match split_lib sp with
-	  | (_,[_,FrozenState fs as hd],before) ->
-	      lib_stk := hd::before;
-	      recalc_path_prefix ();
-			set_command_label 0;
-	      unfreeze_summaries fs
-	  | _ -> assert false
-	end
-
-
 (* Misc *)
 
 let mp_of_global ref =
diff --git a/library/lib.mli b/library/lib.mli
index 0d6eb34b..45c598aa 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -62,17 +62,6 @@ val add_leaves : Names.identifier -> Libobject.obj list -> Libnames.object_name
 
 val add_frozen_state : unit -> unit
 
-(** Adds a "dummy" entry in lib_stk with a unique new label number. *)
-val mark_end_of_command : unit -> unit
-
-(** Returns the current label number *)
-val current_command_label : unit -> int
-
-(** [reset_label n] resets [lib_stk] to the label n registered by
-   [mark_end_of_command()]. It forgets the label and anything
-   registered after it. The label should be strictly in the past. *)
-val reset_label : int -> unit
-
 (** {6 ... } *)
 (** The function [contents_after] returns the current library segment,
   starting from a given section path. If not given, the entire segment
@@ -151,16 +140,28 @@ val remove_section_part : Libnames.global_reference -> Names.dir_path
 val open_section : Names.identifier -> unit
 val close_section : unit -> unit
 
-(** {6 Backtracking (undo). } *)
+(** {6 Backtracking } *)
 
-val reset_to : Libnames.object_name -> unit
-val reset_name : Names.identifier Util.located -> unit
-val remove_name : Names.identifier Util.located -> unit
-val reset_mod : Names.identifier Util.located -> unit
+(** NB: The next commands are low-level ones, do not use them directly
+    otherwise the command history stack in [Backtrack] will be out-of-sync.
+    Also note that [reset_initial] is now [reset_label first_command_label] *)
 
-(** [back n] resets to the place corresponding to the {% $ %}n{% $ %}-th call of
-   [mark_end_of_command] (counting backwards) *)
-val back : int -> unit
+(** Adds a "dummy" entry in lib_stk with a unique new label number. *)
+val mark_end_of_command : unit -> unit
+
+(** Returns the current label number *)
+val current_command_label : unit -> int
+
+(** The first label number *)
+val first_command_label : int
+
+(** [reset_label n] resets [lib_stk] to the label n registered by
+   [mark_end_of_command()]. It forgets anything registered after
+   this label. The label should be strictly in the past. *)
+val reset_label : int -> unit
+
+(** search the label registered immediately before adding some definition *)
+val label_before_name : Names.identifier Util.located -> int
 
 (** {6 We can get and set the state of the operations (used in [States]). } *)
 
@@ -171,10 +172,6 @@ val unfreeze : frozen -> unit
 
 val init : unit -> unit
 
-val declare_initial_state : unit -> unit
-val reset_initial : unit -> unit
-
-
 (** XML output hooks *)
 val set_xml_open_section : (Names.identifier -> unit) -> unit
 val set_xml_close_section : (Names.identifier -> unit) -> unit