From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 14 Oct 2010 17:51:11 +0200
Subject: Imported Upstream version 8.3

---
 library/impargs.ml  | 318 +++++++++++++++++++++++++++++++++-------------------
 library/impargs.mli |  28 +++--
 library/states.ml   |   6 +-
 library/states.mli  |   4 +-
 4 files changed, 227 insertions(+), 129 deletions(-)

(limited to 'library')

diff --git a/library/impargs.ml b/library/impargs.ml
index 2aff1dec..e695be3c 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: impargs.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: impargs.ml 13499 2010-10-05 10:08:44Z herbelin $ *)
 
 open Util
 open Names
@@ -29,14 +29,12 @@ open Namegen
 type implicits_flags = {
   auto : bool;                     (* automatic or manual only *)
   strict : bool;                   (* true = strict *)
-  strongly_strict : bool;            (* true = strongly strict *)
+  strongly_strict : bool;          (* true = strongly strict *)
   reversible_pattern : bool;
   contextual : bool;               (* true = contextual *)
   maximal : bool
 }
 
-(* les implicites sont stricts par défaut en v8 *)
-
 let implicit_args = ref {
   auto = false;
   strict = true;
@@ -198,6 +196,17 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
   in
   frec true (env,1) m; acc
 
+let rec is_rigid_head t = match kind_of_term t with
+  | Rel _ | Evar _ -> false
+  | Ind _ | Const _ | Var _ | Sort _ -> true
+  | Case (_,_,f,_) -> is_rigid_head f
+  | App (f,args) ->
+      (match kind_of_term f with
+	| Fix ((fi,i),_) -> is_rigid_head (args.(fi.(i)))
+	| _ -> is_rigid_head f)
+  | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _
+  | Prod _ | Meta _ | Cast _ -> assert false
+
 (* calcule la liste des arguments implicites *)
 
 let find_displayed_name_in all avoid na b =
@@ -207,6 +216,7 @@ let find_displayed_name_in all avoid na b =
     compute_displayed_name_in (RenamingElsewhereFor b) avoid na b
 
 let compute_implicits_gen strict strongly_strict revpat contextual all env t =
+  let rigid = ref true in
   let rec aux env avoid n names t =
     let t = whd_betadeltaiota env t in
     match kind_of_term t with
@@ -215,6 +225,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
 	  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)
       | _ ->
+	  rigid := is_rigid_head t;
 	  let names = List.rev names in
 	  let v = Array.map (fun na -> na,None) (Array.of_list names) in
 	  if contextual then
@@ -225,8 +236,66 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
     | Prod (na,a,b) ->
 	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
-	Array.to_list v
-    | _ -> []
+	!rigid, Array.to_list v
+    | _ -> true, []
+
+let compute_implicits_flags env f all t =
+  compute_implicits_gen
+    (f.strict or f.strongly_strict) f.strongly_strict
+    f.reversible_pattern f.contextual all env t
+
+let compute_auto_implicits env flags enriching t =
+  if enriching then compute_implicits_flags env flags true t
+  else compute_implicits_gen false false false true true env t
+
+(* Extra information about implicit arguments *)
+
+type maximal_insertion = bool (* true = maximal contextual insertion *)
+type force_inference = bool (* true = always infer, never turn into evar/subgoal *)
+
+type implicit_status =
+    (* None = Not implicit *)
+    (identifier * implicit_explanation * (maximal_insertion * force_inference)) option
+
+type implicit_side_condition = DefaultImpArgs | LessArgsThan of int
+
+type implicits_list = implicit_side_condition * implicit_status list
+
+let is_status_implicit = function
+  | None -> false
+  | _ -> true
+
+let name_of_implicit = function
+  | None -> anomaly "Not an implicit argument"
+  | Some (id,_,_) -> id
+
+let maximal_insertion_of = function
+  | Some (_,_,(b,_)) -> b
+  | None -> anomaly "Not an implicit argument"
+
+let force_inference_of = function
+  | Some (_, _, (_, b)) -> b
+  | None -> anomaly "Not an implicit argument"
+
+(* [in_ctx] means we know the expected type, [n] is the index of the argument *)
+let is_inferable_implicit in_ctx n = function
+  | None -> false
+  | Some (_,DepRigid (Hyp p),_) -> in_ctx or n >= p
+  | Some (_,DepFlex (Hyp p),_) -> false
+  | Some (_,DepFlexAndRigid (_,Hyp q),_) -> in_ctx or n >= q
+  | Some (_,DepRigid Conclusion,_) -> in_ctx
+  | Some (_,DepFlex Conclusion,_) -> false
+  | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx
+  | Some (_,Manual,_) -> true
+
+let positions_of_implicits (_,impls) =
+  let rec aux n = function
+      [] -> []
+    | Some _ :: l -> n :: aux (n+1) l
+    | None :: l -> aux (n+1) l
+  in aux 1 impls
+
+(* Manage user-given implicit arguments *)
 
 let rec prepare_implicits f = function
   | [] -> []
@@ -236,11 +305,6 @@ let rec prepare_implicits f = function
       Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
   | _::imps -> None :: prepare_implicits f imps
 
-let compute_implicits_flags env f all t =
-  compute_implicits_gen
-    (f.strict or f.strongly_strict) f.strongly_strict
-    f.reversible_pattern f.contextual all env t
-
 let set_implicit id imp insmax =
   (id,(match imp with None -> Manual | Some imp -> imp),insmax)
 
@@ -249,11 +313,20 @@ let rec assoc_by_pos k = function
   | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl
   | [] -> raise Not_found
 
-let compute_manual_implicits env flags t enriching l =
-  let autoimps =
-    if enriching then compute_implicits_flags env flags true t
-    else compute_implicits_gen false false false true true env t in
-  let n = List.length autoimps in
+let check_correct_manual_implicits autoimps l =
+  List.iter (function
+    | ExplByName id,(b,fi,forced) ->
+	if not forced then
+	  error ("Wrong or non-dependent implicit argument name: "^(string_of_id id)^".")
+    | ExplByPos (i,_id),_t ->
+	if i<1 or i>List.length autoimps then
+	  error ("Bad implicit argument number: "^(string_of_int i)^".")
+	else
+	  errorlabstrm ""
+	    (str "Cannot set implicit argument number " ++ int i ++
+	      str ": it has no name.")) l
+
+let set_manual_implicits env flags enriching autoimps l =
   let try_forced k l =
     try
       let (id, (b, fi, fo)), l' = assoc_by_pos k l in
@@ -264,7 +337,7 @@ let compute_manual_implicits env flags t enriching l =
     with Not_found -> l, None
   in
   if not (list_distinct l) then
-    error ("Some parameters are referred more than once");
+    error ("Some parameters are referred more than once.");
   (* Compare with automatic implicits to recover printing data and names *)
   let rec merge k l = function
   | (Name id,imp)::imps ->
@@ -287,81 +360,28 @@ let compute_manual_implicits env flags t enriching l =
 	forced :: merge (k+1) l' imps
   | [] when l = [] -> []
   | [] ->
-      List.iter (function
-	| ExplByName id,(b,fi,forced) ->
-	    if not forced then
-	      error ("Wrong or not dependent implicit argument name: "^(string_of_id id))
-	| ExplByPos (i,_id),_t ->
-	    if i<1 or i>n then
-	      error ("Bad implicit argument number: "^(string_of_int i))
-	    else
-	      errorlabstrm ""
-		(str "Cannot set implicit argument number " ++ int i ++
-		    str ": it has no name"))
-	l; []
+      check_correct_manual_implicits autoimps l;
+      []
   in
   merge 1 l autoimps
 
-let const v _ = v
-
-let compute_implicits_auto env f manual t =
+let compute_semi_auto_implicits env f manual t =
   match manual with
   | [] ->
-      if not f.auto then []
-      else let l = compute_implicits_flags env f false t in
-	     prepare_implicits f l
-  | _ -> compute_manual_implicits env f t f.auto manual
-
-let compute_implicits env t = compute_implicits_auto env !implicit_args [] t
-
-type maximal_insertion = bool (* true = maximal contextual insertion *)
-type force_inference = bool (* true = always infer, never turn into evar/subgoal *)
-
-type implicit_status =
-    (* None = Not implicit *)
-    (identifier * implicit_explanation * (maximal_insertion * force_inference)) option
-
-type implicits_list = implicit_status list
-
-let is_status_implicit = function
-  | None -> false
-  | _ -> true
-
-let name_of_implicit = function
-  | None -> anomaly "Not an implicit argument"
-  | Some (id,_,_) -> id
-
-let maximal_insertion_of = function
-  | Some (_,_,(b,_)) -> b
-  | None -> anomaly "Not an implicit argument"
+      if not f.auto then [DefaultImpArgs, []]
+      else let _,l = compute_implicits_flags env f false t in
+	     [DefaultImpArgs, prepare_implicits f l]
+  | _ ->
+      let _,autoimpls = compute_auto_implicits env f f.auto t in
+      [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual]
 
-let force_inference_of = function
-  | Some (_, _, (_, b)) -> b
-  | None -> anomaly "Not an implicit argument"
-
-(* [in_ctx] means we know the expected type, [n] is the index of the argument *)
-let is_inferable_implicit in_ctx n = function
-  | None -> false
-  | Some (_,DepRigid (Hyp p),_) -> in_ctx or n >= p
-  | Some (_,DepFlex (Hyp p),_) -> false
-  | Some (_,DepFlexAndRigid (_,Hyp q),_) -> in_ctx or n >= q
-  | Some (_,DepRigid Conclusion,_) -> in_ctx
-  | Some (_,DepFlex Conclusion,_) -> false
-  | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx
-  | Some (_,Manual,_) -> true
-
-let positions_of_implicits =
-  let rec aux n = function
-      [] -> []
-    | Some _ :: l -> n :: aux (n+1) l
-    | None :: l -> aux (n+1) l
-  in aux 1
+let compute_implicits env t = compute_semi_auto_implicits env !implicit_args [] t
 
 (*s Constants. *)
 
 let compute_constant_implicits flags manual cst =
   let env = Global.env () in
-  compute_implicits_auto env flags manual (Typeops.type_of_constant env cst)
+  compute_semi_auto_implicits env flags manual (Typeops.type_of_constant env cst)
 
 (*s Inductives and constructors. Their implicit arguments are stored
    in an array, indexed by the inductive number, of pairs $(i,v)$ where
@@ -381,9 +401,9 @@ let compute_mib_implicits flags manual kn =
   let imps_one_inductive i mip =
     let ind = (kn,i) in
     let ar = type_of_inductive env (mib,mip) in
-    ((IndRef ind,compute_implicits_auto env flags manual ar),
+    ((IndRef ind,compute_semi_auto_implicits env flags manual ar),
      Array.mapi (fun j c ->
-       (ConstructRef (ind,j+1),compute_implicits_auto env_ar flags manual c))
+       (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar flags manual c))
        mip.mind_nf_lc)
   in
   Array.mapi imps_one_inductive mib.mind_packets
@@ -398,7 +418,7 @@ let compute_all_mib_implicits flags manual kn =
 let compute_var_implicits flags manual id =
   let env = Global.env () in
   let (_,_,ty) = lookup_named id env in
-  compute_implicits_auto env flags manual ty
+  compute_semi_auto_implicits env flags manual ty
 
 (* Implicits of a global reference. *)
 
@@ -412,24 +432,21 @@ let compute_global_implicits flags manual = function
 
 (* Merge a manual explicitation with an implicit_status list *)
 
-let merge_impls oldimpls newimpls =
-  let (before, news), olds =
-    let len = List.length newimpls - List.length oldimpls in
-      if len >= 0 then list_split_at len newimpls, oldimpls
-      else
-	let before, after = list_split_at (-len) oldimpls in
-	  (before, newimpls), after
-  in
-    before @ (List.map2 (fun orig ni ->
-      match orig with
-      | Some (_, Manual, _) -> orig
-      | _ -> ni) olds news)
+let merge_impls (cond,oldimpls) (_,newimpls) =
+  let oldimpls,usersuffiximpls = list_chop (List.length newimpls) oldimpls in
+  cond, (List.map2 (fun orig ni ->
+    match orig with
+    | Some (_, Manual, _) -> orig
+    | _ -> ni) oldimpls newimpls)@usersuffiximpls
+
+let merge_impls_list oldimpls newimpls =
+  merge_impls oldimpls newimpls
 
 (* Caching implicits *)
 
 type implicit_interactive_request =
   | ImplAuto
-  | ImplManual of implicit_status list
+  | ImplManual of int
 
 type implicit_discharge_request =
   | ImplLocal
@@ -441,7 +458,7 @@ type implicit_discharge_request =
 let implicits_table = ref Refmap.empty
 
 let implicits_of_global ref =
-  try Refmap.find ref !implicits_table with Not_found -> []
+  try Refmap.find ref !implicits_table with Not_found -> [DefaultImpArgs,[]]
 
 let cache_implicits_decl (ref,imps) =
   implicits_table := Refmap.add ref imps !implicits_table
@@ -467,23 +484,35 @@ let section_segment_of_reference = function
       section_segment_of_mutual_inductive kn
   | _ -> []
 
+let adjust_side_condition p = function
+  | LessArgsThan n -> LessArgsThan (n+p)
+  | DefaultImpArgs -> DefaultImpArgs
+
+let add_section_impls vars extra_impls (cond,impls) =
+  let p = List.length vars - List.length extra_impls in
+  adjust_side_condition p cond, extra_impls @ impls
+
 let discharge_implicits (_,(req,l)) =
   match req with
   | ImplLocal -> None
   | ImplInteractive (ref,flags,exp) ->
       let vars = section_segment_of_reference ref in
       let ref' = if isVarRef ref then ref else pop_global_reference ref in
-      let l' = [ref', impls_of_context vars @ snd (List.hd l)] in
+      let extra_impls = impls_of_context vars in
+      let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
       Some (ImplInteractive (ref',flags,exp),l')
   | ImplConstant (con,flags) ->
       let con' = pop_con con in
-      let l' = [ConstRef con',impls_of_context (section_segment_of_constant con) @ snd (List.hd l)] in
+      let vars = section_segment_of_constant con in
+      let extra_impls = impls_of_context vars in
+      let l' = [ConstRef con',List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
 	Some (ImplConstant (con',flags),l')
   | ImplMutualInductive (kn,flags) ->
       let l' = List.map (fun (gr, l) ->
 	let vars = section_segment_of_reference gr in
+	let extra_impls = impls_of_context vars in
 	((if isVarRef gr then gr else pop_global_reference gr),
-	 impls_of_context vars @ l)) l
+	 List.map (add_section_impls vars extra_impls) l)) l
       in
 	Some (ImplMutualInductive (pop_kn kn,flags),l')
 
@@ -493,13 +522,13 @@ let rebuild_implicits (req,l) =
   | ImplConstant (con,flags) ->
       let oldimpls = snd (List.hd l) in
       let newimpls = compute_constant_implicits flags [] con in
-      req, [ConstRef con, merge_impls oldimpls newimpls]
+      req, [ConstRef con, List.map2 merge_impls oldimpls newimpls]
   | ImplMutualInductive (kn,flags) ->
       let newimpls = compute_all_mib_implicits flags [] kn in
       let rec aux olds news =
 	match olds, news with
 	| (_, oldimpls) :: old, (gr, newimpls) :: tl ->
-	    (gr, merge_impls oldimpls newimpls) :: aux old tl
+	    (gr, List.map2 merge_impls oldimpls newimpls) :: aux old tl
 	| [], [] -> []
 	| _, _ -> assert false
       in req, aux l newimpls
@@ -510,17 +539,16 @@ let rebuild_implicits (req,l) =
       | ImplAuto ->
 	  let oldimpls = snd (List.hd l) in
 	  let newimpls = compute_global_implicits flags [] ref in
-	    [ref,merge_impls oldimpls newimpls]
-      | ImplManual m ->
+	    [ref,List.map2 merge_impls oldimpls newimpls]
+      | ImplManual userimplsize ->
 	  let oldimpls = snd (List.hd l) in
-	  let auto =
-	    if flags.auto then
-	      let newimpls = compute_global_implicits flags [] ref in
-		merge_impls oldimpls newimpls
-	    else oldimpls
-	  in
-	  let l' = merge_impls auto m in
-	  [ref,l']
+	  if flags.auto then
+	    let newimpls = List.hd (compute_global_implicits flags [] ref) in
+	    let p = List.length (snd newimpls) - userimplsize in
+	    let newimpls = on_snd (list_firstn p) newimpls in
+	    [ref,List.map (fun o -> merge_impls o newimpls) oldimpls]
+	  else
+	    [ref,oldimpls]
 
 let classify_implicits (req,_ as obj) =
   if req = ImplLocal then Dispose else Substitute obj
@@ -566,23 +594,58 @@ let declare_mib_implicits kn =
 type manual_explicitation = Topconstr.explicitation * (bool * bool * bool)
 
 let compute_implicits_with_manual env typ enriching l =
-  compute_manual_implicits env !implicit_args typ enriching l
+  let _,autoimpls = compute_auto_implicits env !implicit_args enriching typ in
+  set_manual_implicits env !implicit_args enriching autoimpls l
+
+let check_inclusion l =
+  (* Check strict inclusion *)
+  let rec aux = function
+    | n1::(n2::_ as nl) ->
+	if n1 <= n2 then
+	  error "Sequences of implicit arguments must be of different lengths";
+	aux nl
+    | _ -> () in
+  aux (List.map (fun (imps,_) -> List.length imps) l)
+
+let check_rigidity isrigid =
+  if not isrigid then
+    errorlabstrm "" (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.")
 
 let declare_manual_implicits local ref ?enriching l =
   let flags = !implicit_args in
   let env = Global.env () in
   let t = Global.type_of_global ref in
   let enriching = Option.default flags.auto enriching in
-  let l' = compute_manual_implicits env flags t enriching l in
+  let isrigid,autoimpls = compute_auto_implicits env flags enriching t in
+  let l' = match l with
+    | [] -> assert false
+    | [l] ->
+	[DefaultImpArgs, set_manual_implicits env flags enriching autoimpls l]
+    | _ ->
+	check_rigidity isrigid;
+	let l = List.map (fun imps -> (imps,List.length imps)) l in
+	let l = Sort.list (fun (_,n1) (_,n2) -> n1 > n2) l in
+	check_inclusion l;
+	let nargs = List.length autoimpls in
+	List.map (fun (imps,n) ->
+	  (LessArgsThan (nargs-n),
+	   set_manual_implicits env flags enriching autoimpls imps)) l in
   let req =
     if is_local local ref then ImplLocal
-    else ImplInteractive(ref,flags,ImplManual l')
+    else ImplInteractive(ref,flags,ImplManual (List.length autoimpls))
   in
     add_anonymous_leaf (inImplicits (req,[ref,l']))
 
 let maybe_declare_manual_implicits local ref ?enriching l =
   if l = [] then ()
-  else declare_manual_implicits local ref ?enriching l
+  else declare_manual_implicits local ref ?enriching [l]
+
+let extract_impargs_data impls =
+  let rec aux p = function
+    | (DefaultImpArgs, imps)::_ -> [None,imps]
+    | (LessArgsThan n, imps)::l -> (Some (p,n),imps) :: aux (n+1) l
+    | [] -> [] in
+  aux 0 impls
 
 let lift_implicits n =
   List.map (fun x ->
@@ -590,6 +653,27 @@ let lift_implicits n =
 	ExplByPos (k, id) -> ExplByPos (k + n, id), snd x
       | _ -> x)
 
+let make_implicits_list l = [DefaultImpArgs, l]
+
+let rec drop_first_implicits p l =
+  if p = 0 then l else match l with
+  | _,[] as x -> x
+  | DefaultImpArgs,imp::impls ->
+      drop_first_implicits (p-1) (DefaultImpArgs,impls)
+  | LessArgsThan n,imp::impls ->
+      let n = if is_status_implicit imp then n-1 else n in
+      drop_first_implicits (p-1) (LessArgsThan n,impls)
+
+let rec select_impargs_size n = function
+  | [] -> [] (* Tolerance for (DefaultImpArgs,[]) *)
+  | [_, impls] | (DefaultImpArgs, impls)::_ -> impls
+  | (LessArgsThan p, impls)::l ->
+      if n <= p then impls else select_impargs_size n l
+
+let rec select_stronger_impargs = function
+  | [] -> [] (* Tolerance for (DefaultImpArgs,[]) *)
+  | (_,impls)::_ -> impls
+
 (*s Registration as global tables *)
 
 let init () = implicits_table := Refmap.empty
diff --git a/library/impargs.mli b/library/impargs.mli
index 1c27d9f5..0b0ae544 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: impargs.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: impargs.mli 13499 2010-10-05 10:08:44Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -51,7 +51,10 @@ type implicit_explanation =
   | Manual
 
 type implicit_status = (identifier * implicit_explanation * (bool * bool)) option
-type implicits_list = implicit_status list
+
+type implicit_side_condition
+
+type implicits_list = implicit_side_condition * implicit_status list
 
 val is_status_implicit : implicit_status -> bool
 val is_inferable_implicit : bool -> int -> implicit_status -> bool
@@ -63,7 +66,7 @@ val positions_of_implicits : implicits_list -> int list
 
 (* Computation of the positions of arguments automatically inferable
    for an object of the given type in the given env *)
-val compute_implicits : env -> types -> implicits_list
+val compute_implicits : env -> types -> implicits_list list
 
 (* A [manual_explicitation] is a tuple of a positional or named explicitation with
    maximal insertion, force inference and force usage flags. Forcing usage makes
@@ -71,7 +74,7 @@ val compute_implicits : env -> types -> implicits_list
 type manual_explicitation = Topconstr.explicitation * (bool * bool * bool)
 
 val compute_implicits_with_manual : env -> types -> bool ->
-  manual_explicitation list -> implicits_list
+  manual_explicitation list -> implicit_status list
 
 (*s Computation of implicits (done using the global environment). *)
 
@@ -88,22 +91,33 @@ val declare_implicits : bool -> global_reference -> unit
    Unsets implicits if [l] is empty. *)
 
 val declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
-  manual_explicitation list -> unit
+  manual_explicitation list list -> unit
 
 (* If the list is empty, do nothing, otherwise declare the implicits. *)
 
 val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
   manual_explicitation list -> unit
 
-val implicits_of_global : global_reference -> implicits_list
+val implicits_of_global : global_reference -> implicits_list list
+
+val extract_impargs_data :
+  implicits_list list -> ((int * int) option * implicit_status list) list
 
 val lift_implicits : int -> manual_explicitation list -> manual_explicitation list
 
 val merge_impls : implicits_list -> implicits_list -> implicits_list
 
+val make_implicits_list : implicit_status list -> implicits_list list
+
+val drop_first_implicits : int -> implicits_list -> implicits_list
+
+val select_impargs_size : int -> implicits_list list -> implicit_status list
+
+val select_stronger_impargs : implicits_list list -> implicit_status list
+
 type implicit_interactive_request =
   | ImplAuto
-  | ImplManual of implicit_status list
+  | ImplManual of int
 
 type implicit_discharge_request =
   | ImplLocal
diff --git a/library/states.ml b/library/states.ml
index 3af2bcd7..5fc26045 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: states.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: states.ml 13431 2010-09-18 08:15:29Z herbelin $ *)
 
 open System
 
@@ -30,12 +30,12 @@ let (extern_state,intern_state) =
 
 (* Rollback. *)
 
-let with_heavy_rollback f x =
+let with_heavy_rollback f h x =
   let st = freeze () in
   try
     f x
   with reraise ->
-    (unfreeze st; raise reraise)
+    let e = h reraise in (unfreeze st; raise e)
 
 let with_state_protection f x =
   let st = freeze () in
diff --git a/library/states.mli b/library/states.mli
index 198e1632..b6bdff8b 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: states.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: states.mli 13431 2010-09-18 08:15:29Z herbelin $ i*)
 
 (*s States of the system. In that module, we provide functions to get
   and set the state of the whole system. Internally, it is done by
@@ -24,7 +24,7 @@ val unfreeze : state -> unit
   state of the whole system as it was before the evaluation if an exception
   is raised. *)
 
-val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b
+val with_heavy_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b
 
 (*s [with_state_protection f x] applies [f] to [x] and restores the
   state of the whole system as it was before the evaluation of f *)
-- 
cgit v1.2.3