summaryrefslogtreecommitdiff
path: root/contrib/extraction
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /contrib/extraction
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'contrib/extraction')
-rw-r--r--contrib/extraction/common.ml47
-rw-r--r--contrib/extraction/extraction.ml183
-rw-r--r--contrib/extraction/haskell.ml22
-rw-r--r--contrib/extraction/miniml.mli17
-rw-r--r--contrib/extraction/mlutil.ml87
-rw-r--r--contrib/extraction/mlutil.mli18
-rw-r--r--contrib/extraction/modutil.ml48
-rw-r--r--contrib/extraction/modutil.mli4
-rw-r--r--contrib/extraction/ocaml.ml13
-rw-r--r--contrib/extraction/test/.depend1417
-rw-r--r--contrib/extraction/test/Makefile4
-rw-r--r--contrib/extraction/test/custom/Adalloc4
-rw-r--r--contrib/extraction/test/custom/Lsort4
-rw-r--r--contrib/extraction/test/custom/Map4
-rw-r--r--contrib/extraction/test/custom/Mapcard4
-rw-r--r--contrib/extraction/test/custom/Mapiter4
16 files changed, 1182 insertions, 698 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 8d8438dc..346201ec 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: common.ml 7651 2005-12-16 03:19:20Z letouzey $ i*)
+(*i $Id: common.ml 8930 2006-06-09 02:14:34Z letouzey $ i*)
open Pp
open Util
@@ -112,7 +112,8 @@ let contents_first_level mp =
| Extraction.Term -> add false (id_of_label l))
| (_, SPBmind mib) ->
Array.iter
- (fun mip -> if mip.mind_sort <> (Prop Null) then begin
+ (fun mip -> if snd (Inductive.mind_arity mip) <> InProp
+ then begin
add upper_type mip.mind_typename;
Array.iter (add true) mip.mind_consnames
end)
@@ -267,8 +268,6 @@ module StdParams = struct
let globals () = !global_ids
- (* TODO: remettre des conditions [lang () = Haskell] disant de qualifier. *)
-
let unquote s =
if lang () <> Scheme then s
else
@@ -288,23 +287,31 @@ module StdParams = struct
let mp = modpath_of_r r in
let ls =
if mp = List.hd mpl then [s] (* simpliest situation *)
- else
- try (* has [mp] something in common with one of those in [mpl] ? *)
- let pref = common_prefix_from_list mp mpl in
- (*i TODO: possibilité de clash i*)
- list_firstn ((mp_length mp)-(mp_length pref)+1) ls
- with Not_found -> (* [mp] is othogonal with every element of [mp]. *)
- let base = base_mp mp in
- if !modular &&
- (at_toplevel mp) &&
- not (Refset.mem r !to_qualify) &&
- not (clash base [] s mpl)
- then snd (list_sep_last ls)
- else ls
+ else match lang () with
+ | Scheme -> [s] (* no modular Scheme extraction... *)
+ | Toplevel -> [s] (* idem *)
+ | Haskell ->
+ if !modular then
+ ls (* for the moment we always qualify in modular Haskell *)
+ else [s]
+ | Ocaml ->
+ try (* has [mp] something in common with one of those in [mpl] ? *)
+ let pref = common_prefix_from_list mp mpl in
+ (*i TODO: possibilité de clash i*)
+ list_firstn ((mp_length mp)-(mp_length pref)+1) ls
+ with Not_found -> (* [mp] is othogonal with every element of [mp]. *)
+ let base = base_mp mp in
+ if !modular &&
+ (at_toplevel mp) &&
+ not (Refset.mem r !to_qualify) &&
+ not (clash base [] s mpl)
+ then snd (list_sep_last ls)
+ else ls
in
add_module_contents mp s; (* update the visible environment *)
str (dottify ls)
+ (* The next function is used only in Ocaml extraction...*)
let pp_module mpl mp =
let ls =
if !modular
@@ -393,15 +400,15 @@ let print_structure_to_file f prm struc =
in
let print_dummys =
(struct_ast_search ((=) MLdummy) struc,
- struct_type_search Tdummy struc,
- struct_type_search Tunknown struc)
+ struct_type_search Mlutil.isDummy struc,
+ struct_type_search ((=) Tunknown) struc)
in
let print_magic =
if lang () <> Haskell then false
else struct_ast_search (function MLmagic _ -> true | _ -> false) struc
in
(* print the implementation *)
- let cout = option_app (fun (f,_) -> open_out f) f in
+ let cout = option_map (fun (f,_) -> open_out f) f in
let ft = match cout with
| None -> !Pp_control.std_ft
| Some cout -> Pp_control.with_output_to cout in
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index a4bf973d..e97df539 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extraction.ml 7639 2005-12-02 10:01:15Z gregoire $ i*)
+(*i $Id: extraction.ml 8931 2006-06-09 07:43:37Z letouzey $ i*)
(*i*)
open Util
@@ -35,6 +35,9 @@ exception I of inductive_info
to avoid loops in [extract_inductive] *)
let internal_call = ref KNset.empty
+(* A set of all fixpoint functions currently being extracted *)
+let current_fixpoints = ref ([] : constant list)
+
let none = Evd.empty
let type_of env c = Retyping.get_type_of env none (strip_outer_cast c)
@@ -80,6 +83,14 @@ let rec flag_of_type env t =
let is_default env t = (flag_of_type env t = (Info, Default))
+exception NotDefault of kill_reason
+
+let check_default env t =
+ match flag_of_type env t with
+ | _,TypeScheme -> raise (NotDefault Ktype)
+ | Logic,_ -> raise (NotDefault Kother)
+ | _ -> ()
+
let is_info_scheme env t = (flag_of_type env t = (Info, TypeScheme))
(*s [type_sign] gernerates a signature aimed at treating a type application. *)
@@ -87,7 +98,8 @@ let is_info_scheme env t = (flag_of_type env t = (Info, TypeScheme))
let rec type_sign env c =
match kind_of_term (whd_betadeltaiota env none c) with
| Prod (n,t,d) ->
- (is_info_scheme env t)::(type_sign (push_rel_assum (n,t) env) d)
+ (if is_info_scheme env t then Keep else Kill Kother)
+ :: (type_sign (push_rel_assum (n,t) env) d)
| _ -> []
let rec type_scheme_nb_args env c =
@@ -105,8 +117,8 @@ let rec type_sign_vl env c =
match kind_of_term (whd_betadeltaiota env none c) with
| Prod (n,t,d) ->
let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in
- if not (is_info_scheme env t) then false::s, vl
- else true::s, (next_ident_away (id_of_name n) vl) :: vl
+ if not (is_info_scheme env t) then Kill Kother::s, vl
+ else Keep::s, (next_ident_away (id_of_name n) vl) :: vl
| _ -> [],[]
let rec nb_default_params env c =
@@ -126,8 +138,8 @@ let rec nb_default_params env c =
let db_from_sign s =
let rec make i acc = function
| [] -> acc
- | true :: l -> make (i+1) (i::acc) l
- | false :: l -> make i (0::acc) l
+ | Keep :: l -> make (i+1) (i::acc) l
+ | Kill _ :: l -> make i (0::acc) l
in make 1 [] s
(*s Create a type variable context from indications taken from
@@ -150,8 +162,8 @@ let rec db_from_ind dbmap i =
let parse_ind_args si args relmax =
let rec parse i j = function
| [] -> Intmap.empty
- | false :: s -> parse (i+1) j s
- | true :: s ->
+ | Kill _ :: s -> parse (i+1) j s
+ | Keep :: s ->
(match kind_of_term args.(i-1) with
| Rel k -> Intmap.add (relmax+1-k) j (parse (i+1) (j+1) s)
| _ -> parse (i+1) (j+1) s)
@@ -167,6 +179,7 @@ let parse_ind_args si args relmax =
(* [j] stands for the next ML type var. [j=0] means we do not
generate ML type var anymore (in subterms for example). *)
+
let rec extract_type env db j c args =
match kind_of_term (whd_betaiotazeta c) with
| App (d, args') ->
@@ -183,19 +196,24 @@ let rec extract_type env db j c args =
| (Info, Default) ->
(* Standard case: two [extract_type] ... *)
let mld = extract_type env' (0::db) j d [] in
- if type_eq (mlt_env env) mld Tdummy then Tdummy
- else Tarr (extract_type env db 0 t [], mld)
+ (match expand env mld with
+ | Tdummy d -> Tdummy d
+ | _ -> Tarr (extract_type env db 0 t [], mld))
| (Info, TypeScheme) when j > 0 ->
(* A new type var. *)
let mld = extract_type env' (j::db) (j+1) d [] in
- if type_eq (mlt_env env) mld Tdummy then Tdummy
- else Tarr (Tdummy, mld)
- | _ ->
+ (match expand env mld with
+ | Tdummy d -> Tdummy d
+ | _ -> Tarr (Tdummy Ktype, mld))
+ | _,lvl ->
let mld = extract_type env' (0::db) j d [] in
- if type_eq (mlt_env env) mld Tdummy then Tdummy
- else Tarr (Tdummy, mld))
- | Sort _ -> Tdummy (* The two logical cases. *)
- | _ when sort_of env (applist (c, args)) = InProp -> Tdummy
+ (match expand env mld with
+ | Tdummy d -> Tdummy d
+ | _ ->
+ let reason = if lvl=TypeScheme then Ktype else Kother in
+ Tarr (Tdummy reason, mld)))
+ | Sort _ -> Tdummy Ktype (* The two logical cases. *)
+ | _ when sort_of env (applist (c, args)) = InProp -> Tdummy Kother
| Rel n ->
(match lookup_rel n env with
| (_,Some t,_) -> extract_type env db j (lift n t) args
@@ -222,7 +240,7 @@ let rec extract_type env db j c args =
(* The more precise is [mlt'], extracted after reduction *)
(* The shortest is [mlt], which use abbreviations *)
(* If possible, we take [mlt], otherwise [mlt']. *)
- if type_eq (mlt_env env) mlt mlt' then mlt else mlt')
+ if expand env mlt = expand env mlt' then mlt else mlt')
| _ -> (* only other case here: Info, Default, i.e. not an ML type *)
(match cb.const_body with
| None -> Tunknown (* Brutal approximation ... *)
@@ -242,7 +260,7 @@ let rec extract_type env db j c args =
and extract_maybe_type env db c =
let t = whd_betadeltaiota env none (type_of env c) in
if isSort t then extract_type env db 0 c []
- else if sort_of env t = InProp then Tdummy else Tunknown
+ else if sort_of env t = InProp then Tdummy Kother else Tunknown
(*s Auxiliary function dealing with type application.
Precondition: [r] is a type scheme represented by the signature [s],
@@ -251,7 +269,7 @@ and extract_maybe_type env db c =
and extract_type_app env db (r,s) args =
let ml_args =
List.fold_right
- (fun (b,c) a -> if b then
+ (fun (b,c) a -> if b=Keep then
let p = List.length (fst (splay_prod env none (type_of env c))) in
let db = iterate (fun l -> 0 :: l) p db in
(extract_type_scheme env db c p) :: a
@@ -301,9 +319,10 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
(* their type var list. *)
let packets =
Array.map
- (fun mip ->
- let b = mip.mind_sort <> (Prop Null) in
- let s,v = if b then type_sign_vl env mip.mind_nf_arity else [],[] in
+ (fun mip ->
+ let b = snd (mind_arity mip) <> InProp in
+ let ar = Inductive.type_of_inductive (mib,mip) in
+ let s,v = if b then type_sign_vl env ar else [],[] in
let t = Array.make (Array.length mip.mind_nf_lc) [] in
{ ip_typename = mip.mind_typename;
ip_consnames = mip.mind_consnames;
@@ -341,7 +360,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
if p.ip_logical then raise (I Standard);
if Array.length p.ip_types <> 1 then raise (I Standard);
let typ = p.ip_types.(0) in
- let l = List.filter (type_neq (mlt_env env) Tdummy) typ in
+ let l = List.filter (fun t -> not (isDummy (expand env t))) typ in
if List.length l = 1 && not (type_mem_kn kn (List.hd l))
then raise (I Singleton);
if l = [] then raise (I Standard);
@@ -365,14 +384,15 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
let rec select_fields l typs = match l,typs with
| [],[] -> []
| (Name id)::l, typ::typs ->
- if type_eq (mlt_env env) Tdummy typ then select_fields l typs
+ if isDummy (expand env typ) then select_fields l typs
else
let knp = make_con mp d (label_of_id id) in
- if not (List.mem false (type_to_sign (mlt_env env) typ)) then
+ if not (List.exists isKill (type2signature env typ))
+ then
projs := Cset.add knp !projs;
(ConstRef knp) :: (select_fields l typs)
| Anonymous::l, typ::typs ->
- if type_eq (mlt_env env) Tdummy typ then select_fields l typs
+ if isDummy (expand env typ) then select_fields l typs
else error_record r
| _ -> assert false
in
@@ -381,7 +401,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
(* Is this record officially declared with its projections ? *)
(* If so, we use this information. *)
begin try
- let n = nb_default_params env mip0.mind_nf_arity in
+ let n = nb_default_params env (Inductive.type_of_inductive(mib,mip0))
+ in
List.iter
(option_iter
(fun kn -> if Cset.mem kn !projs then add_projection n kn))
@@ -439,9 +460,9 @@ and mlt_env env r = match r with
| _ -> None))
| _ -> None
-let type_expand env = type_expand (mlt_env env)
-let type_neq env = type_neq (mlt_env env)
-let type_to_sign env = type_to_sign (mlt_env env)
+and expand env = type_expand (mlt_env env)
+and type2signature env = type_to_signature (mlt_env env)
+let type2sign env = type_to_sign (mlt_env env)
let type_expunge env = type_expunge (mlt_env env)
(*s Extraction of the type of a constant. *)
@@ -478,10 +499,9 @@ let rec extract_term env mle mlt c args =
in extract_term env mle mlt d' []
| [] ->
let env' = push_rel_assum (Name id, t) env in
- let id, a =
- if is_default env t
- then id, new_meta ()
- else dummy_name, Tdummy in
+ let id, a = try check_default env t; id, new_meta()
+ with NotDefault d -> dummy_name, Tdummy d
+ in
let b = new_meta () in
(* If [mlt] cannot be unified with an arrow type, then magic! *)
let magic = needs_magic (mlt, Tarr (a, b)) in
@@ -491,15 +511,16 @@ let rec extract_term env mle mlt c args =
let id = id_of_name n in
let env' = push_rel (Name id, Some c1, t1) env in
let args' = List.map (lift 1) args in
- if is_default env t1 then
+ (try
+ check_default env t1;
let a = new_meta () in
let c1' = extract_term env mle a c1 [] in
(* The type of [c1'] is generalized and stored in [mle]. *)
let mle' = Mlenv.push_gen mle a in
MLletin (id, c1', extract_term env' mle' mlt c2 args')
- else
- let mle' = Mlenv.push_std_type mle Tdummy in
- ast_pop (extract_term env' mle' mlt c2 args')
+ with NotDefault d ->
+ let mle' = Mlenv.push_std_type mle (Tdummy d) in
+ ast_pop (extract_term env' mle' mlt c2 args'))
| Const kn ->
extract_cst_app env mle mlt kn args
| Construct cp ->
@@ -521,8 +542,10 @@ let rec extract_term env mle mlt c args =
(*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *)
and extract_maybe_term env mle mlt c =
- if is_default env (type_of env c) then extract_term env mle mlt c []
- else put_magic (mlt, Tdummy) MLdummy
+ try check_default env (type_of env c);
+ extract_term env mle mlt c []
+ with NotDefault d ->
+ put_magic (mlt, Tdummy d) MLdummy
(*s Generic way to deal with an application. *)
@@ -540,7 +563,7 @@ and extract_app env mle mlt mk_head args =
and make_mlargs env e s args typs =
let l = ref s in
- let keep () = match !l with [] -> true | b :: s -> l:=s; b in
+ let keep () = match !l with [] -> true | b :: s -> l:=s; b=Keep in
let rec f = function
| [], [] -> []
| a::la, t::lt when keep() -> extract_maybe_term env e t a :: (f (la,lt))
@@ -553,19 +576,25 @@ and make_mlargs env e s args typs =
and extract_cst_app env mle mlt kn args =
(* First, the [ml_schema] of the constant, in expanded version. *)
let nb,t = record_constant_type env kn None in
- let schema = nb, type_expand env t in
+ let schema = nb, expand env t in
+ (* Can we instantiate types variables for this constant ? *)
+ (* In Ocaml, inside the definition of this constant, the answer is no. *)
+ let instantiated =
+ if lang () = Ocaml && List.mem kn !current_fixpoints then var2var' (snd schema)
+ else instantiation schema
+ in
(* Then the expected type of this constant. *)
- let metas = List.map new_meta args in
+ let a = new_meta () in
(* We compare stored and expected types in two steps. *)
(* First, can [kn] be applied to all args ? *)
- let a = new_meta () in
- let magic1 = needs_magic (type_recomp (metas, a), instantiation schema) in
+ let metas = List.map new_meta args in
+ let magic1 = needs_magic (type_recomp (metas, a), instantiated) in
(* Second, is the resulting type compatible with the expected type [mlt] ? *)
let magic2 = needs_magic (a, mlt) in
(* The internal head receives a magic if [magic1] *)
let head = put_magic_if magic1 (MLglob (ConstRef kn)) in
(* Now, the extraction of the arguments. *)
- let s = type_to_sign env (snd schema) in
+ let s = type2signature env (snd schema) in
let ls = List.length s in
let la = List.length args in
let mla = make_mlargs env mle s args metas in
@@ -580,8 +609,8 @@ and extract_cst_app env mle mlt kn args =
in
(* Different situations depending of the number of arguments: *)
if ls = 0 then put_magic_if magic2 head
- else if List.mem true s then
- if la >= ls || not (List.mem false s)
+ else if List.mem Keep s then
+ if la >= ls || not (List.exists isKill s)
then
put_magic_if (magic2 && not magic1) (MLapp (head, mla))
else
@@ -590,12 +619,17 @@ and extract_cst_app env mle mlt kn args =
let s' = list_lastn ls' s in
let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
put_magic_if magic2 (anonym_or_dummy_lams (MLapp (head, mla)) s')
- else
+ else if List.mem (Kill Kother) s then
(* In the special case of always false signature, one dummy lam is left. *)
(* So a [MLdummy] is left accordingly. *)
if la >= ls
then put_magic_if (magic2 && not magic1) (MLapp (head, MLdummy :: mla))
else put_magic_if magic2 (dummy_lams head (ls-la-1))
+ else (* s is made only of [Kill Ktype] *)
+ if la >= ls
+ then put_magic_if (magic2 && not magic1) (MLapp (head, mla))
+ else put_magic_if magic2 (dummy_lams head (ls-la))
+
(*s Extraction of an inductive constructor applied to arguments. *)
@@ -613,12 +647,12 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
let params_nb = mi.ind_nparams in
let oi = mi.ind_packets.(i) in
let nb_tvars = List.length oi.ip_vars
- and types = List.map (type_expand env) oi.ip_types.(j-1) in
+ and types = List.map (expand env) oi.ip_types.(j-1) in
let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in
let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
let type_cons = instantiation (nb_tvars, type_cons) in
(* Then, the usual variables [s], [ls], [la], ... *)
- let s = List.map (type_neq env Tdummy) types in
+ let s = List.map (type2sign env) types in
let ls = List.length s in
let la = List.length args in
assert (la <= ls + params_nb);
@@ -671,8 +705,8 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
(* Logical singleton case: *)
(* [match c with C i j k -> t] becomes [t'] *)
assert (br_size = 1);
- let s = iterate (fun l -> false :: l) ni.(0) [] in
- let mlt = iterate (fun t -> Tarr (Tdummy, t)) ni.(0) mlt in
+ let s = iterate (fun l -> Kill Kother :: l) ni.(0) [] in
+ let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni.(0) mlt in
let e = extract_maybe_term env mle mlt br.(0) in
snd (case_expunge s e)
end
@@ -686,10 +720,10 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
(* The extraction of each branch. *)
let extract_branch i =
(* The types of the arguments of the corresponding constructor. *)
- let f t = type_subst_vect metas (type_expand env t) in
+ let f t = type_subst_vect metas (expand env t) in
let l = List.map f oi.ip_types.(i) in
(* the corresponding signature *)
- let s = List.map (type_neq env Tdummy) oi.ip_types.(i) in
+ let s = List.map (type2sign env) oi.ip_types.(i) in
(* Extraction of the branch (in functional form). *)
let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in
(* We suppress dummy arguments according to signature. *)
@@ -745,8 +779,8 @@ let extract_std_constant env kn body typ =
let t = snd (record_constant_type env kn (Some typ)) in
(* The real type [t']: without head lambdas, expanded, *)
(* and with [Tvar] translated to [Tvar'] (not instantiable). *)
- let l,t' = type_decomp (type_expand env (var2var' t)) in
- let s = List.map (type_neq env Tdummy) l in
+ let l,t' = type_decomp (expand env (var2var' t)) in
+ let s = List.map (type2sign env) l in
(* The initial ML environment. *)
let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in
(* Decomposing the top level lambdas of [body]. *)
@@ -762,10 +796,12 @@ let extract_std_constant env kn body typ =
let extract_fixpoint env vkn (fi,ti,ci) =
let n = Array.length vkn in
- let types = Array.make n Tdummy
+ let types = Array.make n (Tdummy Kother)
and terms = Array.make n MLdummy in
+ let kns = Array.to_list vkn in
+ current_fixpoints := kns;
(* for replacing recursive calls [Rel ..] by the corresponding [Const]: *)
- let sub = List.rev_map mkConst (Array.to_list vkn) in
+ let sub = List.rev_map mkConst kns in
for i = 0 to n-1 do
if sort_of env ti.(i) <> InProp then begin
let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in
@@ -773,6 +809,7 @@ let extract_fixpoint env vkn (fi,ti,ci) =
types.(i) <- t;
end
done;
+ current_fixpoints := [];
Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types)
let extract_constant env kn cb =
@@ -790,12 +827,14 @@ let extract_constant env kn cb =
if not (is_custom r) then warning_info_ax r;
let t = snd (record_constant_type env kn (Some typ)) in
Dterm (r, MLaxiom, type_expunge env t)
- | (Logic,TypeScheme) -> warning_log_ax r; Dtype (r, [], Tdummy)
- | (Logic,Default) -> warning_log_ax r; Dterm (r, MLdummy, Tdummy))
+ | (Logic,TypeScheme) ->
+ warning_log_ax r; Dtype (r, [], Tdummy Ktype)
+ | (Logic,Default) ->
+ warning_log_ax r; Dterm (r, MLdummy, Tdummy Kother))
| Some body ->
(match flag_of_type env typ with
- | (Logic, Default) -> Dterm (r, MLdummy, Tdummy)
- | (Logic, TypeScheme) -> Dtype (r, [], Tdummy)
+ | (Logic, Default) -> Dterm (r, MLdummy, Tdummy Kother)
+ | (Logic, TypeScheme) -> Dtype (r, [], Tdummy Ktype)
| (Info, Default) ->
let e,t = extract_std_constant env kn (force body) typ in
Dterm (r,e,t)
@@ -809,8 +848,8 @@ let extract_constant_spec env kn cb =
let r = ConstRef kn in
let typ = cb.const_type in
match flag_of_type env typ with
- | (Logic, TypeScheme) -> Stype (r, [], Some Tdummy)
- | (Logic, Default) -> Sval (r, Tdummy)
+ | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
+ | (Logic, Default) -> Sval (r, Tdummy Kother)
| (Info, TypeScheme) ->
let s,vl = type_sign_vl env typ in
(match cb.const_body with
@@ -826,7 +865,7 @@ let extract_constant_spec env kn cb =
let extract_inductive env kn =
let ind = extract_ind env kn in
add_recursors env kn;
- let f l = List.filter (type_neq env Tdummy) l in
+ let f l = List.filter (fun t -> not (isDummy (expand env t))) l in
let packets =
Array.map (fun p -> { p with ip_types = Array.map f p.ip_types })
ind.ind_packets
@@ -853,19 +892,19 @@ let constant_kind env cb =
(*s Is a [ml_decl] logical ? *)
let logical_decl = function
- | Dterm (_,MLdummy,Tdummy) -> true
- | Dtype (_,[],Tdummy) -> true
+ | Dterm (_,MLdummy,Tdummy _) -> true
+ | Dtype (_,[],Tdummy _) -> true
| Dfix (_,av,tv) ->
(array_for_all ((=) MLdummy) av) &&
- (array_for_all ((=) Tdummy) tv)
+ (array_for_all isDummy tv)
| Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
| _ -> false
(*s Is a [ml_spec] logical ? *)
let logical_spec = function
- | Stype (_, [], Some Tdummy) -> true
- | Sval (_,Tdummy) -> true
+ | Stype (_, [], Some (Tdummy _)) -> true
+ | Sval (_,Tdummy _) -> true
| Sind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
| _ -> false
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index c4ed364a..f924396c 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: haskell.ml 7653 2005-12-16 04:12:26Z letouzey $ i*)
+(*i $Id: haskell.ml 8930 2006-06-09 02:14:34Z letouzey $ i*)
(*s Production of Haskell syntax. *)
@@ -106,7 +106,7 @@ let rec pp_type par vl t =
| Tarr (t1,t2) ->
pp_par par
(pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
- | Tdummy -> str "()"
+ | Tdummy _ -> str "()"
| Tunknown -> str "()"
| Taxiom -> str "() -- AXIOM TO BE REALIZED\n"
in
@@ -210,7 +210,7 @@ and pp_function env f t =
(f ++ pr_binding (List.rev bl) ++
str " =" ++ fnl () ++ str " " ++
hov 2 (pp_expr false env' [] t'))
-
+
(*s Pretty-printing of inductive types declaration. *)
let pp_comment s = str "-- " ++ s ++ fnl ()
@@ -289,12 +289,16 @@ let pp_decl mpl =
else str "=" ++ spc () ++ pp_type false l t
in
hov 2 (str "type " ++ pp_global r ++ spc () ++ st) ++ fnl () ++ fnl ()
- | Dfix (rv, defs,_) ->
- let ppv = Array.map pp_global rv in
- prlist_with_sep (fun () -> fnl () ++ fnl ())
- (fun (pi,ti) -> pp_function (empty_env ()) pi ti)
- (List.combine (Array.to_list ppv) (Array.to_list defs))
- ++ fnl () ++ fnl ()
+ | Dfix (rv, defs, typs) ->
+ let max = Array.length rv in
+ let rec iter i =
+ if i = max then mt ()
+ else
+ let e = pp_global rv.(i) in
+ e ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl ()
+ ++ pp_function (empty_env ()) e defs.(i) ++ fnl () ++ fnl ()
+ ++ iter (i+1)
+ in iter 0
| Dterm (r, a, t) ->
if is_inline_custom r then mt ()
else
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index cf722e4e..e34abe02 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: miniml.mli 6064 2004-09-06 07:49:51Z letouzey $ i*)
+(*i $Id: miniml.mli 8724 2006-04-20 09:57:01Z letouzey $ i*)
(*s Target language for extraction: a core ML called MiniML. *)
@@ -18,11 +18,18 @@ open Libnames
(* The [signature] type is used to know how many arguments a CIC
object expects, and what these arguments will become in the ML
object. *)
+
+(* We eliminate from terms: 1) types 2) logical parts.
+ [Kother] stands both for logical or unknown reason. *)
+
+type kill_reason = Ktype | Kother
+
+type sign = Keep | Kill of kill_reason
+
-(* Convention: outmost lambda/product gives the head of the list,
- and [true] means that the argument is to be kept. *)
+(* Convention: outmost lambda/product gives the head of the list. *)
-type signature = bool list
+type signature = sign list
(*s ML type expressions. *)
@@ -32,7 +39,7 @@ type ml_type =
| Tvar of int
| Tvar' of int (* same as Tvar, used to avoid clash *)
| Tmeta of ml_meta (* used during ML type reconstruction *)
- | Tdummy
+ | Tdummy of kill_reason
| Tunknown
| Taxiom
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index facab18e..6bfedce5 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: mlutil.ml 7574 2005-11-17 15:48:45Z letouzey $ i*)
+(*i $Id: mlutil.ml 8886 2006-06-01 13:53:45Z letouzey $ i*)
(*i*)
open Pp
@@ -111,7 +111,7 @@ let rec mgu = function
List.iter mgu (List.combine l l')
| Tvar i, Tvar j when i = j -> ()
| Tvar' i, Tvar' j when i = j -> ()
- | Tdummy, Tdummy -> ()
+ | Tdummy _, Tdummy _ -> ()
| Tunknown, Tunknown -> ()
| _ -> raise Impossible
@@ -252,7 +252,6 @@ type abbrev_map = global_reference -> ml_type option
(*s Delta-reduction of type constants everywhere in a ML type [t].
[env] is a function of type [ml_type_env]. *)
-
let type_expand env t =
let rec expand = function
| Tmeta {contents = Some t} -> expand t
@@ -281,34 +280,39 @@ let type_weak_expand env t =
| a -> a
in expand t
-(*s Equality over ML types modulo delta-reduction *)
-
-let type_eq env t t' = (type_expand env t = type_expand env t')
-
-let type_neq env t t' = (type_expand env t <> type_expand env t')
-
(*s Generating a signature from a ML type. *)
-let type_to_sign env t =
+let type_to_sign env t = match type_expand env t with
+ | Tdummy d -> Kill d
+ | _ -> Keep
+
+let type_to_signature env t =
let rec f = function
| Tmeta {contents = Some t} -> f t
- | Tarr (a,b) -> (Tdummy <> a) :: (f b)
+ | Tarr (Tdummy d, b) -> Kill d :: f b
+ | Tarr (_, b) -> Keep :: f b
| _ -> []
in f (type_expand env t)
+let isKill = function Kill _ -> true | _ -> false
+
+let isDummy = function Tdummy _ -> true | _ -> false
+
+let sign_of_id i = if i = dummy_name then Kill Kother else Keep
+
(*s Removing [Tdummy] from the top level of a ML type. *)
let type_expunge env t =
- let s = type_to_sign env t in
+ let s = type_to_signature env t in
if s = [] then t
- else if List.mem true s then
+ else if List.mem Keep s then
let rec f t s =
- if List.mem false s then
+ if List.exists isKill s then
match t with
| Tmeta {contents = Some t} -> f t s
| Tarr (a,b) ->
let t = f b (List.tl s) in
- if List.hd s then Tarr (a, t) else t
+ if List.hd s = Keep then Tarr (a, t) else t
| Tglob (r,l) ->
(match env r with
| Some mlt -> f (type_subst_list l mlt) s
@@ -316,7 +320,9 @@ let type_expunge env t =
| _ -> assert false
else t
in f t s
- else Tarr (Tdummy, snd (type_decomp (type_weak_expand env t)))
+ else if List.mem (Kill Kother) s then
+ Tarr (Tdummy Kother, snd (type_decomp (type_weak_expand env t)))
+ else snd (type_decomp (type_weak_expand env t))
(*S Generic functions over ML ast terms. *)
@@ -536,8 +542,8 @@ let rec dummy_lams a = function
let rec anonym_or_dummy_lams a = function
| [] -> a
- | true :: s -> MLlam(anonymous, anonym_or_dummy_lams a s)
- | false :: s -> MLlam(dummy_name, anonym_or_dummy_lams a s)
+ | Keep :: s -> MLlam(anonymous, anonym_or_dummy_lams a s)
+ | Kill _ :: s -> MLlam(dummy_name, anonym_or_dummy_lams a s)
(*S Operations concerning eta. *)
@@ -550,8 +556,8 @@ let rec eta_args n =
let rec eta_args_sign n = function
| [] -> []
- | true :: s -> (MLrel n) :: (eta_args_sign (n-1) s)
- | false :: s -> eta_args_sign (n-1) s
+ | Keep :: s -> (MLrel n) :: (eta_args_sign (n-1) s)
+ | Kill _ :: s -> eta_args_sign (n-1) s
(*s This one tests [MLrel (n+k); ... ;MLrel (1+k)] *)
@@ -820,33 +826,33 @@ let rec post_simpl = function
(*S Local prop elimination. *)
(* We try to eliminate as many [prop] as possible inside an [ml_ast]. *)
-(*s In a list, it selects only the elements corresponding to a [true]
+(*s In a list, it selects only the elements corresponding to a [Keep]
in the boolean list [l]. *)
let rec select_via_bl l args = match l,args with
| [],_ -> args
- | true::l,a::args -> a :: (select_via_bl l args)
- | false::l,a::args -> select_via_bl l args
+ | Keep::l,a::args -> a :: (select_via_bl l args)
+ | Kill _::l,a::args -> select_via_bl l args
| _ -> assert false
-(*s [kill_some_lams] removes some head lambdas according to the bool list [bl].
+(*s [kill_some_lams] removes some head lambdas according to the signature [bl].
This list is build on the identifier list model: outermost lambda
- is on the right. [true] means "to keep" and [false] means "to eliminate".
+ is on the right.
[Rels] corresponding to removed lambdas are supposed not to occur, and
the other [Rels] are made correct via a [gen_subst].
Output is not directly a [ml_ast], compose with [named_lams] if needed. *)
let kill_some_lams bl (ids,c) =
let n = List.length bl in
- let n' = List.fold_left (fun n b -> if b then (n+1) else n) 0 bl in
+ let n' = List.fold_left (fun n b -> if b=Keep then (n+1) else n) 0 bl in
if n = n' then ids,c
else if n' = 0 then [],ast_lift (-n) c
else begin
let v = Array.make n MLdummy in
let rec parse_ids i j = function
| [] -> ()
- | true :: l -> v.(i) <- MLrel j; parse_ids (i+1) (j+1) l
- | false :: l -> parse_ids (i+1) j l
+ | Keep :: l -> v.(i) <- MLrel j; parse_ids (i+1) (j+1) l
+ | Kill _ :: l -> parse_ids (i+1) j l
in parse_ids 0 1 bl ;
select_via_bl bl ids, gen_subst v (n'-n) c
end
@@ -857,8 +863,8 @@ let kill_some_lams bl (ids,c) =
let kill_dummy_lams c =
let ids,c = collect_lams c in
- let bl = List.map ((<>) dummy_name) ids in
- if (List.mem true bl) && (List.mem false bl) then
+ let bl = List.map sign_of_id ids in
+ if (List.mem Keep bl) && (List.exists isKill bl) then
let ids',c = kill_some_lams bl (ids,c) in
ids, named_lams ids' c
else raise Impossible
@@ -866,7 +872,7 @@ let kill_dummy_lams c =
(*s [eta_expansion_sign] takes a function [fun idn ... id1 -> c]
and a signature [s] and builds a eta-long version. *)
-(* For example, if [s = [true;true;false;true]] then the output is :
+(* For example, if [s = [Keep;Keep;Kill Prop;Keep]] then the output is :
[fun idn ... id1 x x _ x -> (c' 4 3 __ 1)] with [c' = lift 4 c] *)
let eta_expansion_sign s (ids,c) =
@@ -874,13 +880,13 @@ let eta_expansion_sign s (ids,c) =
| [] ->
let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels
in ids, MLapp (ast_lift (i-1) c, a)
- | true :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l
- | false :: l -> abs (dummy_name :: ids) (MLdummy :: rels) (i+1) l
+ | Keep :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l
+ | Kill _ :: l -> abs (dummy_name :: ids) (MLdummy :: rels) (i+1) l
in abs ids [] 1 s
(*s If [s = [b1; ... ; bn]] then [case_expunge] decomposes [e]
in [n] lambdas (with eta-expansion if needed) and removes all dummy lambdas
- corresponding to [false] in [s]. *)
+ corresponding to [Del] in [s]. *)
let case_expunge s e =
let m = List.length s in
@@ -892,13 +898,14 @@ let case_expunge s e =
(*s [term_expunge] takes a function [fun idn ... id1 -> c]
and a signature [s] and remove dummy lams. The difference
with [case_expunge] is that we here leave one dummy lambda
- if all lambdas are dummy. *)
+ if all lambdas are logical dummy. *)
let term_expunge s (ids,c) =
if s = [] then c
else
let ids,c = kill_some_lams (List.rev s) (ids,c) in
- if ids = [] then MLlam (dummy_name, ast_lift 1 c)
+ if ids = [] && List.mem (Kill Kother) s then
+ MLlam (dummy_name, ast_lift 1 c)
else named_lams ids c
(*s [kill_dummy_args ids t0 t] looks for occurences of [t0] in [t] and
@@ -907,7 +914,7 @@ let term_expunge s (ids,c) =
let kill_dummy_args ids t0 t =
let m = List.length ids in
- let bl = List.rev_map ((<>) dummy_name) ids in
+ let bl = List.rev_map sign_of_id ids in
let rec killrec n = function
| MLapp(e, a) when e = ast_lift n t0 ->
let k = max 0 (m - (List.length a)) in
@@ -974,7 +981,8 @@ let general_optimize_fix f ids n args m c =
let v = Array.make n 0 in
for i=0 to (n-1) do v.(i)<-i done;
let aux i = function
- | MLrel j when v.(j-1)>=0 -> v.(j-1)<-(-i-1)
+ | MLrel j when v.(j-1)>=0 ->
+ if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1)
| _ -> raise Impossible
in list_iter_i aux args;
let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in
@@ -1001,8 +1009,7 @@ let optimize_fix a =
-> a'
| MLfix(_,[|f|],[|c|]) ->
(try general_optimize_fix f ids n args m c
- with Impossible ->
- named_lams ids (MLapp (MLfix (0,[|f|],[|c|]),args)))
+ with Impossible -> a)
| _ -> a)
| _ -> a
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 1ba1df64..a55caaf2 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: mlutil.mli 6303 2004-11-16 12:37:40Z sacerdot $ i*)
+(*i $Id: mlutil.mli 8724 2006-04-20 09:57:01Z letouzey $ i*)
open Util
open Names
@@ -62,13 +62,15 @@ val var2var' : ml_type -> ml_type
type abbrev_map = global_reference -> ml_type option
val type_expand : abbrev_map -> ml_type -> ml_type
-val type_eq : abbrev_map -> ml_type -> ml_type -> bool
-val type_neq : abbrev_map -> ml_type -> ml_type -> bool
-val type_to_sign : abbrev_map -> ml_type -> bool list
+val type_to_sign : abbrev_map -> ml_type -> sign
+val type_to_signature : abbrev_map -> ml_type -> signature
val type_expunge : abbrev_map -> ml_type -> ml_type
-val case_expunge : bool list -> ml_ast -> identifier list * ml_ast
-val term_expunge : bool list -> identifier list * ml_ast -> ml_ast
+val isDummy : ml_type -> bool
+val isKill : sign -> bool
+
+val case_expunge : signature -> ml_ast -> identifier list * ml_ast
+val term_expunge : signature -> identifier list * ml_ast -> ml_ast
(*s Special identifiers. [dummy_name] is to be used for dead code
@@ -86,9 +88,9 @@ val collect_n_lams : int -> ml_ast -> identifier list * ml_ast
val nb_lams : ml_ast -> int
val dummy_lams : ml_ast -> int -> ml_ast
-val anonym_or_dummy_lams : ml_ast -> bool list -> ml_ast
+val anonym_or_dummy_lams : ml_ast -> signature -> ml_ast
-val eta_args_sign : int -> bool list -> ml_ast list
+val eta_args_sign : int -> signature -> ml_ast list
(*s Utility functions over ML terms. *)
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index ff8daf46..46d4a5a6 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modutil.ml 7632 2005-12-01 14:35:21Z letouzey $ i*)
+(*i $Id: modutil.ml 8724 2006-04-20 09:57:01Z letouzey $ i*)
open Names
open Declarations
@@ -252,40 +252,40 @@ let struct_get_references_list struc =
exception Found
-let rec ast_search t a =
- if t a then raise Found else ast_iter (ast_search t) a
+let rec ast_search f a =
+ if f a then raise Found else ast_iter (ast_search f) a
-let decl_ast_search t = function
- | Dterm (_,a,_) -> ast_search t a
- | Dfix (_,c,_) -> Array.iter (ast_search t) c
+let decl_ast_search f = function
+ | Dterm (_,a,_) -> ast_search f a
+ | Dfix (_,c,_) -> Array.iter (ast_search f) c
| _ -> ()
-let struct_ast_search t s =
- try struct_iter (decl_ast_search t) (fun _ -> ()) s; false
+let struct_ast_search f s =
+ try struct_iter (decl_ast_search f) (fun _ -> ()) s; false
with Found -> true
-let rec type_search t = function
- | Tarr (a,b) -> type_search t a; type_search t b
- | Tglob (r,l) -> List.iter (type_search t) l
- | u -> if t = u then raise Found
+let rec type_search f = function
+ | Tarr (a,b) -> type_search f a; type_search f b
+ | Tglob (r,l) -> List.iter (type_search f) l
+ | u -> if f u then raise Found
-let decl_type_search t = function
+let decl_type_search f = function
| Dind (_,{ind_packets=p}) ->
Array.iter
- (fun {ip_types=v} -> Array.iter (List.iter (type_search t)) v) p
- | Dterm (_,_,u) -> type_search t u
- | Dfix (_,_,v) -> Array.iter (type_search t) v
- | Dtype (_,_,u) -> type_search t u
+ (fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p
+ | Dterm (_,_,u) -> type_search f u
+ | Dfix (_,_,v) -> Array.iter (type_search f) v
+ | Dtype (_,_,u) -> type_search f u
-let spec_type_search t = function
+let spec_type_search f = function
| Sind (_,{ind_packets=p}) ->
Array.iter
- (fun {ip_types=v} -> Array.iter (List.iter (type_search t)) v) p
- | Stype (_,_,ot) -> option_iter (type_search t) ot
- | Sval (_,u) -> type_search t u
+ (fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p
+ | Stype (_,_,ot) -> option_iter (type_search f) ot
+ | Sval (_,u) -> type_search f u
-let struct_type_search t s =
- try struct_iter (decl_type_search t) (spec_type_search t) s; false
+let struct_type_search f s =
+ try struct_iter (decl_type_search f) (spec_type_search f) s; false
with Found -> true
@@ -359,7 +359,7 @@ let dfix_to_mlfix rv av i =
let rec optim prm s = function
| [] -> []
- | (Dtype (r,_,Tdummy) | Dterm(r,MLdummy,_)) as d :: l ->
+ | (Dtype (r,_,Tdummy _) | Dterm(r,MLdummy,_)) as d :: l ->
if List.mem r prm.to_appear then d :: (optim prm s l) else optim prm s l
| Dterm (r,t,typ) :: l ->
let t = normalize (ast_glob_subst !s t) in
diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli
index f5208c0d..115a42ca 100644
--- a/contrib/extraction/modutil.mli
+++ b/contrib/extraction/modutil.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modutil.mli 7632 2005-12-01 14:35:21Z letouzey $ i*)
+(*i $Id: modutil.mli 8724 2006-04-20 09:57:01Z letouzey $ i*)
open Names
open Declarations
@@ -44,7 +44,7 @@ val add_labels_mp : module_path -> label list -> module_path
(*s Functions upon ML modules. *)
val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool
-val struct_type_search : ml_type -> ml_structure -> bool
+val struct_type_search : (ml_type -> bool) -> ml_structure -> bool
type do_ref = global_reference -> unit
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index a0620d72..483da236 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ocaml.ml 7632 2005-12-01 14:35:21Z letouzey $ i*)
+(*i $Id: ocaml.ml 8930 2006-06-09 02:14:34Z letouzey $ i*)
(*s Production of Ocaml syntax. *)
@@ -196,7 +196,7 @@ let rec pp_type par vl t =
| Tarr (t1,t2) ->
pp_par par
(pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
- | Tdummy -> str "__"
+ | Tdummy _ -> str "__"
| Tunknown -> str "__"
in
hov 0 (pp_rec par t)
@@ -343,13 +343,9 @@ and pp_pat env i pv =
and pp_function env f t =
let bl,t' = collect_lams t in
let bl,env' = push_vars bl env in
- let is_function pv =
- let ktl = array_map_to_list (fun (_,l,t0) -> (List.length l,t0)) pv in
- not (List.exists (fun (k,t0) -> ast_occurs (k+1) t0) ktl)
- in
match t' with
- | MLcase(i,MLrel 1,pv) when i=Standard ->
- if is_function pv then
+ | MLcase(i,MLrel 1,pv) when i=Standard ->
+ if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then
(f ++ pr_binding (List.rev (List.tl bl)) ++
str " = function" ++ fnl () ++
v 0 (str " | " ++ pp_pat env' i pv))
@@ -358,7 +354,6 @@ and pp_function env f t =
str " = match " ++
pr_id (List.hd bl) ++ str " with" ++ fnl () ++
v 0 (str " | " ++ pp_pat env' i pv))
-
| _ -> (f ++ pr_binding (List.rev bl) ++
str " =" ++ fnl () ++ str " " ++
hov 2 (pp_expr false env' [] t'))
diff --git a/contrib/extraction/test/.depend b/contrib/extraction/test/.depend
index 641b50a7..31d46eeb 100644
--- a/contrib/extraction/test/.depend
+++ b/contrib/extraction/test/.depend
@@ -2,110 +2,318 @@ theories/Arith/arith.cmo: theories/Arith/arith.cmi
theories/Arith/arith.cmx: theories/Arith/arith.cmi
theories/Arith/between.cmo: theories/Arith/between.cmi
theories/Arith/between.cmx: theories/Arith/between.cmi
-theories/Arith/bool_nat.cmo: theories/Arith/compare_dec.cmi \
- theories/Init/datatypes.cmi theories/Arith/peano_dec.cmi \
- theories/Init/specif.cmi theories/Bool/sumbool.cmi \
+theories/Arith/bool_nat.cmo: theories/Bool/sumbool.cmi \
+ theories/Init/specif.cmi theories/Arith/peano_dec.cmi \
+ theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi \
theories/Arith/bool_nat.cmi
-theories/Arith/bool_nat.cmx: theories/Arith/compare_dec.cmx \
- theories/Init/datatypes.cmx theories/Arith/peano_dec.cmx \
- theories/Init/specif.cmx theories/Bool/sumbool.cmx \
+theories/Arith/bool_nat.cmx: theories/Bool/sumbool.cmx \
+ theories/Init/specif.cmx theories/Arith/peano_dec.cmx \
+ theories/Init/datatypes.cmx theories/Arith/compare_dec.cmx \
theories/Arith/bool_nat.cmi
-theories/Arith/compare_dec.cmo: theories/Init/datatypes.cmi \
- theories/Init/specif.cmi theories/Arith/compare_dec.cmi
-theories/Arith/compare_dec.cmx: theories/Init/datatypes.cmx \
- theories/Init/specif.cmx theories/Arith/compare_dec.cmi
-theories/Arith/compare.cmo: theories/Arith/compare_dec.cmi \
- theories/Init/datatypes.cmi theories/Init/specif.cmi \
+theories/Arith/compare_dec.cmo: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi
+theories/Arith/compare_dec.cmx: theories/Init/specif.cmx \
+ theories/Init/datatypes.cmx theories/Arith/compare_dec.cmi
+theories/Arith/compare.cmo: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi \
theories/Arith/compare.cmi
-theories/Arith/compare.cmx: theories/Arith/compare_dec.cmx \
- theories/Init/datatypes.cmx theories/Init/specif.cmx \
+theories/Arith/compare.cmx: theories/Init/specif.cmx \
+ theories/Init/datatypes.cmx theories/Arith/compare_dec.cmx \
theories/Arith/compare.cmi
-theories/Arith/div2.cmo: theories/Init/datatypes.cmi theories/Init/peano.cmi \
- theories/Init/specif.cmi theories/Arith/div2.cmi
-theories/Arith/div2.cmx: theories/Init/datatypes.cmx theories/Init/peano.cmx \
- theories/Init/specif.cmx theories/Arith/div2.cmi
-theories/Arith/eqNat.cmo: theories/Init/datatypes.cmi \
- theories/Init/specif.cmi theories/Arith/eqNat.cmi
-theories/Arith/eqNat.cmx: theories/Init/datatypes.cmx \
- theories/Init/specif.cmx theories/Arith/eqNat.cmi
-theories/Arith/euclid.cmo: theories/Arith/compare_dec.cmi \
- theories/Init/datatypes.cmi theories/Init/specif.cmi \
+theories/Arith/div2.cmo: theories/Init/specif.cmi theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi theories/Arith/div2.cmi
+theories/Arith/div2.cmx: theories/Init/specif.cmx theories/Init/peano.cmx \
+ theories/Init/datatypes.cmx theories/Arith/div2.cmi
+theories/Arith/eqNat.cmo: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/Arith/eqNat.cmi
+theories/Arith/eqNat.cmx: theories/Init/specif.cmx \
+ theories/Init/datatypes.cmx theories/Arith/eqNat.cmi
+theories/Arith/euclid.cmo: theories/Init/specif.cmi theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi \
theories/Arith/euclid.cmi
-theories/Arith/euclid.cmx: theories/Arith/compare_dec.cmx \
- theories/Init/datatypes.cmx theories/Init/specif.cmx \
+theories/Arith/euclid.cmx: theories/Init/specif.cmx theories/Init/peano.cmx \
+ theories/Init/datatypes.cmx theories/Arith/compare_dec.cmx \
theories/Arith/euclid.cmi
-theories/Arith/even.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \
+theories/Arith/even.cmo: theories/Init/specif.cmi theories/Init/datatypes.cmi \
theories/Arith/even.cmi
-theories/Arith/even.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \
+theories/Arith/even.cmx: theories/Init/specif.cmx theories/Init/datatypes.cmx \
theories/Arith/even.cmi
-theories/Arith/factorial.cmo: theories/Init/datatypes.cmi \
- theories/Init/peano.cmi theories/Arith/factorial.cmi
-theories/Arith/factorial.cmx: theories/Init/datatypes.cmx \
- theories/Init/peano.cmx theories/Arith/factorial.cmi
+theories/Arith/factorial.cmo: theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi theories/Arith/factorial.cmi
+theories/Arith/factorial.cmx: theories/Init/peano.cmx \
+ theories/Init/datatypes.cmx theories/Arith/factorial.cmi
theories/Arith/gt.cmo: theories/Arith/gt.cmi
theories/Arith/gt.cmx: theories/Arith/gt.cmi
theories/Arith/le.cmo: theories/Arith/le.cmi
theories/Arith/le.cmx: theories/Arith/le.cmi
theories/Arith/lt.cmo: theories/Arith/lt.cmi
theories/Arith/lt.cmx: theories/Arith/lt.cmi
-theories/Arith/max.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \
+theories/Arith/max.cmo: theories/Init/specif.cmi theories/Init/datatypes.cmi \
theories/Arith/max.cmi
-theories/Arith/max.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \
+theories/Arith/max.cmx: theories/Init/specif.cmx theories/Init/datatypes.cmx \
theories/Arith/max.cmi
-theories/Arith/min.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \
+theories/Arith/min.cmo: theories/Init/specif.cmi theories/Init/datatypes.cmi \
theories/Arith/min.cmi
-theories/Arith/min.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \
+theories/Arith/min.cmx: theories/Init/specif.cmx theories/Init/datatypes.cmx \
theories/Arith/min.cmi
theories/Arith/minus.cmo: theories/Arith/minus.cmi
theories/Arith/minus.cmx: theories/Arith/minus.cmi
-theories/Arith/mult.cmo: theories/Init/datatypes.cmi theories/Arith/plus.cmi \
+theories/Arith/mult.cmo: theories/Arith/plus.cmi theories/Init/datatypes.cmi \
theories/Arith/mult.cmi
-theories/Arith/mult.cmx: theories/Init/datatypes.cmx theories/Arith/plus.cmx \
+theories/Arith/mult.cmx: theories/Arith/plus.cmx theories/Init/datatypes.cmx \
theories/Arith/mult.cmi
-theories/Arith/peano_dec.cmo: theories/Init/datatypes.cmi \
- theories/Init/specif.cmi theories/Arith/peano_dec.cmi
-theories/Arith/peano_dec.cmx: theories/Init/datatypes.cmx \
- theories/Init/specif.cmx theories/Arith/peano_dec.cmi
-theories/Arith/plus.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \
+theories/Arith/peano_dec.cmo: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/Arith/peano_dec.cmi
+theories/Arith/peano_dec.cmx: theories/Init/specif.cmx \
+ theories/Init/datatypes.cmx theories/Arith/peano_dec.cmi
+theories/Arith/plus.cmo: theories/Init/specif.cmi theories/Init/datatypes.cmi \
theories/Arith/plus.cmi
-theories/Arith/plus.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \
+theories/Arith/plus.cmx: theories/Init/specif.cmx theories/Init/datatypes.cmx \
theories/Arith/plus.cmi
theories/Arith/wf_nat.cmo: theories/Init/datatypes.cmi \
theories/Arith/wf_nat.cmi
theories/Arith/wf_nat.cmx: theories/Init/datatypes.cmx \
theories/Arith/wf_nat.cmi
-theories/Bool/boolEq.cmo: theories/Init/datatypes.cmi \
- theories/Init/specif.cmi theories/Bool/boolEq.cmi
-theories/Bool/boolEq.cmx: theories/Init/datatypes.cmx \
- theories/Init/specif.cmx theories/Bool/boolEq.cmi
-theories/Bool/bool.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \
+theories/Bool/boolEq.cmo: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/Bool/boolEq.cmi
+theories/Bool/boolEq.cmx: theories/Init/specif.cmx \
+ theories/Init/datatypes.cmx theories/Bool/boolEq.cmi
+theories/Bool/bool.cmo: theories/Init/specif.cmi theories/Init/datatypes.cmi \
theories/Bool/bool.cmi
-theories/Bool/bool.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \
+theories/Bool/bool.cmx: theories/Init/specif.cmx theories/Init/datatypes.cmx \
theories/Bool/bool.cmi
-theories/Bool/bvector.cmo: theories/Bool/bool.cmi theories/Init/datatypes.cmi \
- theories/Init/peano.cmi theories/Bool/bvector.cmi
-theories/Bool/bvector.cmx: theories/Bool/bool.cmx theories/Init/datatypes.cmx \
- theories/Init/peano.cmx theories/Bool/bvector.cmi
+theories/Bool/bvector.cmo: theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi theories/Bool/bool.cmi \
+ theories/Bool/bvector.cmi
+theories/Bool/bvector.cmx: theories/Init/peano.cmx \
+ theories/Init/datatypes.cmx theories/Bool/bool.cmx \
+ theories/Bool/bvector.cmi
theories/Bool/decBool.cmo: theories/Init/specif.cmi theories/Bool/decBool.cmi
theories/Bool/decBool.cmx: theories/Init/specif.cmx theories/Bool/decBool.cmi
-theories/Bool/ifProp.cmo: theories/Init/datatypes.cmi \
- theories/Init/specif.cmi theories/Bool/ifProp.cmi
-theories/Bool/ifProp.cmx: theories/Init/datatypes.cmx \
- theories/Init/specif.cmx theories/Bool/ifProp.cmi
-theories/Bool/sumbool.cmo: theories/Init/datatypes.cmi \
- theories/Init/specif.cmi theories/Bool/sumbool.cmi
-theories/Bool/sumbool.cmx: theories/Init/datatypes.cmx \
- theories/Init/specif.cmx theories/Bool/sumbool.cmi
+theories/Bool/ifProp.cmo: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/Bool/ifProp.cmi
+theories/Bool/ifProp.cmx: theories/Init/specif.cmx \
+ theories/Init/datatypes.cmx theories/Bool/ifProp.cmi
+theories/Bool/sumbool.cmo: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/Bool/sumbool.cmi
+theories/Bool/sumbool.cmx: theories/Init/specif.cmx \
+ theories/Init/datatypes.cmx theories/Bool/sumbool.cmi
theories/Bool/zerob.cmo: theories/Init/datatypes.cmi theories/Bool/zerob.cmi
theories/Bool/zerob.cmx: theories/Init/datatypes.cmx theories/Bool/zerob.cmi
+theories/FSets/decidableTypeEx.cmo: theories/Init/specif.cmi \
+ theories/FSets/orderedTypeEx.cmi theories/FSets/orderedType.cmi \
+ theories/Init/datatypes.cmi theories/FSets/decidableTypeEx.cmi
+theories/FSets/decidableTypeEx.cmx: theories/Init/specif.cmx \
+ theories/FSets/orderedTypeEx.cmx theories/FSets/orderedType.cmx \
+ theories/Init/datatypes.cmx theories/FSets/decidableTypeEx.cmi
+theories/FSets/decidableType.cmo: theories/Init/specif.cmi \
+ theories/FSets/decidableType.cmi
+theories/FSets/decidableType.cmx: theories/Init/specif.cmx \
+ theories/FSets/decidableType.cmi
+theories/FSets/fMapAVL.cmo: theories/Init/wf.cmi theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/Lists/list.cmi \
+ theories/FSets/int.cmi theories/FSets/fMapList.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi theories/FSets/fMapAVL.cmi
+theories/FSets/fMapAVL.cmx: theories/Init/wf.cmx theories/Init/specif.cmx \
+ theories/FSets/orderedType.cmx theories/Lists/list.cmx \
+ theories/FSets/int.cmx theories/FSets/fMapList.cmx \
+ theories/Init/datatypes.cmx theories/NArith/binPos.cmx \
+ theories/ZArith/binInt.cmx theories/FSets/fMapAVL.cmi
+theories/FSets/fMapFacts.cmo: theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/FSets/fMapInterface.cmi \
+ theories/Init/datatypes.cmi theories/FSets/fMapFacts.cmi
+theories/FSets/fMapFacts.cmx: theories/Init/specif.cmx \
+ theories/FSets/orderedType.cmx theories/FSets/fMapInterface.cmx \
+ theories/Init/datatypes.cmx theories/FSets/fMapFacts.cmi
+theories/FSets/fMapInterface.cmo: theories/FSets/orderedType.cmi \
+ theories/Lists/list.cmi theories/Init/datatypes.cmi \
+ theories/FSets/fMapInterface.cmi
+theories/FSets/fMapInterface.cmx: theories/FSets/orderedType.cmx \
+ theories/Lists/list.cmx theories/Init/datatypes.cmx \
+ theories/FSets/fMapInterface.cmi
+theories/FSets/fMapIntMap.cmo: theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/NArith/ndigits.cmi \
+ theories/IntMap/mapiter.cmi theories/IntMap/mapcanon.cmi \
+ theories/IntMap/map.cmi theories/Lists/list.cmi \
+ theories/FSets/fMapList.cmi theories/Init/datatypes.cmi \
+ theories/NArith/binNat.cmi theories/FSets/fMapIntMap.cmi
+theories/FSets/fMapIntMap.cmx: theories/Init/specif.cmx \
+ theories/FSets/orderedType.cmx theories/NArith/ndigits.cmx \
+ theories/IntMap/mapiter.cmx theories/IntMap/mapcanon.cmx \
+ theories/IntMap/map.cmx theories/Lists/list.cmx \
+ theories/FSets/fMapList.cmx theories/Init/datatypes.cmx \
+ theories/NArith/binNat.cmx theories/FSets/fMapIntMap.cmi
+theories/FSets/fMapList.cmo: theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi theories/FSets/fMapList.cmi
+theories/FSets/fMapList.cmx: theories/Init/specif.cmx \
+ theories/FSets/orderedType.cmx theories/Lists/list.cmx \
+ theories/Init/datatypes.cmx theories/FSets/fMapList.cmi
+theories/FSets/fMapPositive.cmo: theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/FSets/fMapPositive.cmi
+theories/FSets/fMapPositive.cmx: theories/Init/specif.cmx \
+ theories/FSets/orderedType.cmx theories/Lists/list.cmx \
+ theories/Init/datatypes.cmx theories/NArith/binPos.cmx \
+ theories/FSets/fMapPositive.cmi
+theories/FSets/fMaps.cmo: theories/FSets/fMaps.cmi
+theories/FSets/fMaps.cmx: theories/FSets/fMaps.cmi
+theories/FSets/fMapWeakFacts.cmo: theories/Init/specif.cmi \
+ theories/Lists/list.cmi theories/FSets/fMapWeakInterface.cmi \
+ theories/Init/datatypes.cmi theories/FSets/fMapWeakFacts.cmi
+theories/FSets/fMapWeakFacts.cmx: theories/Init/specif.cmx \
+ theories/Lists/list.cmx theories/FSets/fMapWeakInterface.cmx \
+ theories/Init/datatypes.cmx theories/FSets/fMapWeakFacts.cmi
+theories/FSets/fMapWeakInterface.cmo: theories/Lists/list.cmi \
+ theories/FSets/decidableType.cmi theories/Init/datatypes.cmi \
+ theories/FSets/fMapWeakInterface.cmi
+theories/FSets/fMapWeakInterface.cmx: theories/Lists/list.cmx \
+ theories/FSets/decidableType.cmx theories/Init/datatypes.cmx \
+ theories/FSets/fMapWeakInterface.cmi
+theories/FSets/fMapWeakList.cmo: theories/Init/specif.cmi \
+ theories/Lists/list.cmi theories/FSets/decidableType.cmi \
+ theories/Init/datatypes.cmi theories/FSets/fMapWeakList.cmi
+theories/FSets/fMapWeakList.cmx: theories/Init/specif.cmx \
+ theories/Lists/list.cmx theories/FSets/decidableType.cmx \
+ theories/Init/datatypes.cmx theories/FSets/fMapWeakList.cmi
+theories/FSets/fMapWeak.cmo: theories/FSets/fMapWeak.cmi
+theories/FSets/fMapWeak.cmx: theories/FSets/fMapWeak.cmi
+theories/FSets/fSetAVL.cmo: theories/Init/wf.cmi theories/Init/specif.cmi \
+ theories/Init/peano.cmi theories/FSets/orderedType.cmi \
+ theories/Lists/list.cmi theories/FSets/int.cmi \
+ theories/FSets/fSetList.cmi theories/Init/datatypes.cmi \
+ theories/NArith/binPos.cmi theories/ZArith/binInt.cmi \
+ theories/FSets/fSetAVL.cmi
+theories/FSets/fSetAVL.cmx: theories/Init/wf.cmx theories/Init/specif.cmx \
+ theories/Init/peano.cmx theories/FSets/orderedType.cmx \
+ theories/Lists/list.cmx theories/FSets/int.cmx \
+ theories/FSets/fSetList.cmx theories/Init/datatypes.cmx \
+ theories/NArith/binPos.cmx theories/ZArith/binInt.cmx \
+ theories/FSets/fSetAVL.cmi
+theories/FSets/fSetBridge.cmo: theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/Lists/list.cmi \
+ theories/FSets/fSetInterface.cmi theories/Init/datatypes.cmi \
+ theories/FSets/fSetBridge.cmi
+theories/FSets/fSetBridge.cmx: theories/Init/specif.cmx \
+ theories/FSets/orderedType.cmx theories/Lists/list.cmx \
+ theories/FSets/fSetInterface.cmx theories/Init/datatypes.cmx \
+ theories/FSets/fSetBridge.cmi
+theories/FSets/fSetEqProperties.cmo: theories/Init/specif.cmi \
+ theories/Setoids/setoid.cmi theories/Init/peano.cmi \
+ theories/FSets/orderedType.cmi theories/FSets/fSetProperties.cmi \
+ theories/FSets/fSetInterface.cmi theories/Init/datatypes.cmi \
+ theories/Bool/bool.cmi theories/FSets/fSetEqProperties.cmi
+theories/FSets/fSetEqProperties.cmx: theories/Init/specif.cmx \
+ theories/Setoids/setoid.cmx theories/Init/peano.cmx \
+ theories/FSets/orderedType.cmx theories/FSets/fSetProperties.cmx \
+ theories/FSets/fSetInterface.cmx theories/Init/datatypes.cmx \
+ theories/Bool/bool.cmx theories/FSets/fSetEqProperties.cmi
+theories/FSets/fSetFacts.cmo: theories/Init/specif.cmi \
+ theories/Setoids/setoid.cmi theories/FSets/orderedType.cmi \
+ theories/FSets/fSetInterface.cmi theories/Init/datatypes.cmi \
+ theories/FSets/fSetFacts.cmi
+theories/FSets/fSetFacts.cmx: theories/Init/specif.cmx \
+ theories/Setoids/setoid.cmx theories/FSets/orderedType.cmx \
+ theories/FSets/fSetInterface.cmx theories/Init/datatypes.cmx \
+ theories/FSets/fSetFacts.cmi
+theories/FSets/fSetInterface.cmo: theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi theories/FSets/fSetInterface.cmi
+theories/FSets/fSetInterface.cmx: theories/Init/specif.cmx \
+ theories/FSets/orderedType.cmx theories/Lists/list.cmx \
+ theories/Init/datatypes.cmx theories/FSets/fSetInterface.cmi
+theories/FSets/fSetList.cmo: theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi theories/FSets/fSetList.cmi
+theories/FSets/fSetList.cmx: theories/Init/specif.cmx \
+ theories/FSets/orderedType.cmx theories/Lists/list.cmx \
+ theories/Init/datatypes.cmx theories/FSets/fSetList.cmi
+theories/FSets/fSetProperties.cmo: theories/Init/specif.cmi \
+ theories/Setoids/setoid.cmi theories/FSets/orderedType.cmi \
+ theories/Lists/list.cmi theories/FSets/fSetInterface.cmi \
+ theories/FSets/fSetFacts.cmi theories/Init/datatypes.cmi \
+ theories/FSets/fSetProperties.cmi
+theories/FSets/fSetProperties.cmx: theories/Init/specif.cmx \
+ theories/Setoids/setoid.cmx theories/FSets/orderedType.cmx \
+ theories/Lists/list.cmx theories/FSets/fSetInterface.cmx \
+ theories/FSets/fSetFacts.cmx theories/Init/datatypes.cmx \
+ theories/FSets/fSetProperties.cmi
+theories/FSets/fSets.cmo: theories/FSets/fSets.cmi
+theories/FSets/fSets.cmx: theories/FSets/fSets.cmi
+theories/FSets/fSetToFiniteSet.cmo: theories/Init/specif.cmi \
+ theories/Setoids/setoid.cmi theories/FSets/orderedTypeEx.cmi \
+ theories/FSets/orderedType.cmi theories/Lists/list.cmi \
+ theories/FSets/fSetProperties.cmi theories/Init/datatypes.cmi \
+ theories/FSets/fSetToFiniteSet.cmi
+theories/FSets/fSetToFiniteSet.cmx: theories/Init/specif.cmx \
+ theories/Setoids/setoid.cmx theories/FSets/orderedTypeEx.cmx \
+ theories/FSets/orderedType.cmx theories/Lists/list.cmx \
+ theories/FSets/fSetProperties.cmx theories/Init/datatypes.cmx \
+ theories/FSets/fSetToFiniteSet.cmi
+theories/FSets/fSetWeakFacts.cmo: theories/Init/specif.cmi \
+ theories/Setoids/setoid.cmi theories/FSets/fSetWeakInterface.cmi \
+ theories/Init/datatypes.cmi theories/FSets/fSetWeakFacts.cmi
+theories/FSets/fSetWeakFacts.cmx: theories/Init/specif.cmx \
+ theories/Setoids/setoid.cmx theories/FSets/fSetWeakInterface.cmx \
+ theories/Init/datatypes.cmx theories/FSets/fSetWeakFacts.cmi
+theories/FSets/fSetWeakInterface.cmo: theories/Lists/list.cmi \
+ theories/FSets/decidableType.cmi theories/Init/datatypes.cmi \
+ theories/FSets/fSetWeakInterface.cmi
+theories/FSets/fSetWeakInterface.cmx: theories/Lists/list.cmx \
+ theories/FSets/decidableType.cmx theories/Init/datatypes.cmx \
+ theories/FSets/fSetWeakInterface.cmi
+theories/FSets/fSetWeakList.cmo: theories/Init/specif.cmi \
+ theories/Lists/list.cmi theories/FSets/decidableType.cmi \
+ theories/Init/datatypes.cmi theories/FSets/fSetWeakList.cmi
+theories/FSets/fSetWeakList.cmx: theories/Init/specif.cmx \
+ theories/Lists/list.cmx theories/FSets/decidableType.cmx \
+ theories/Init/datatypes.cmx theories/FSets/fSetWeakList.cmi
+theories/FSets/fSetWeak.cmo: theories/FSets/fSetWeak.cmi
+theories/FSets/fSetWeak.cmx: theories/FSets/fSetWeak.cmi
+theories/FSets/fSetWeakProperties.cmo: theories/Init/specif.cmi \
+ theories/Setoids/setoid.cmi theories/Lists/list.cmi \
+ theories/FSets/fSetWeakInterface.cmi theories/FSets/fSetWeakFacts.cmi \
+ theories/Init/datatypes.cmi theories/FSets/fSetWeakProperties.cmi
+theories/FSets/fSetWeakProperties.cmx: theories/Init/specif.cmx \
+ theories/Setoids/setoid.cmx theories/Lists/list.cmx \
+ theories/FSets/fSetWeakInterface.cmx theories/FSets/fSetWeakFacts.cmx \
+ theories/Init/datatypes.cmx theories/FSets/fSetWeakProperties.cmi
+theories/FSets/int.cmo: theories/ZArith/zmax.cmi \
+ theories/ZArith/zArith_dec.cmi theories/Init/specif.cmi \
+ theories/NArith/binPos.cmi theories/ZArith/binInt.cmi \
+ theories/FSets/int.cmi
+theories/FSets/int.cmx: theories/ZArith/zmax.cmx \
+ theories/ZArith/zArith_dec.cmx theories/Init/specif.cmx \
+ theories/NArith/binPos.cmx theories/ZArith/binInt.cmx \
+ theories/FSets/int.cmi
+theories/FSets/orderedTypeAlt.cmo: theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/Init/datatypes.cmi \
+ theories/FSets/orderedTypeAlt.cmi
+theories/FSets/orderedTypeAlt.cmx: theories/Init/specif.cmx \
+ theories/FSets/orderedType.cmx theories/Init/datatypes.cmx \
+ theories/FSets/orderedTypeAlt.cmi
+theories/FSets/orderedTypeEx.cmo: theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/Init/datatypes.cmi \
+ theories/Arith/compare_dec.cmi theories/NArith/binPos.cmi \
+ theories/NArith/binNat.cmi theories/ZArith/binInt.cmi \
+ theories/FSets/orderedTypeEx.cmi
+theories/FSets/orderedTypeEx.cmx: theories/Init/specif.cmx \
+ theories/FSets/orderedType.cmx theories/Init/datatypes.cmx \
+ theories/Arith/compare_dec.cmx theories/NArith/binPos.cmx \
+ theories/NArith/binNat.cmx theories/ZArith/binInt.cmx \
+ theories/FSets/orderedTypeEx.cmi
+theories/FSets/orderedType.cmo: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/FSets/orderedType.cmi
+theories/FSets/orderedType.cmx: theories/Init/specif.cmx \
+ theories/Init/datatypes.cmx theories/FSets/orderedType.cmi
theories/Init/datatypes.cmo: theories/Init/datatypes.cmi
theories/Init/datatypes.cmx: theories/Init/datatypes.cmi
theories/Init/logic.cmo: theories/Init/logic.cmi
theories/Init/logic.cmx: theories/Init/logic.cmi
-theories/Init/logic_Type.cmo: theories/Init/datatypes.cmi \
- theories/Init/logic_Type.cmi
-theories/Init/logic_Type.cmx: theories/Init/datatypes.cmx \
- theories/Init/logic_Type.cmi
+theories/Init/logic_Type.cmo: theories/Init/logic_Type.cmi
+theories/Init/logic_Type.cmx: theories/Init/logic_Type.cmi
theories/Init/notations.cmo: theories/Init/notations.cmi
theories/Init/notations.cmx: theories/Init/notations.cmi
theories/Init/peano.cmo: theories/Init/datatypes.cmi theories/Init/peano.cmi
@@ -116,152 +324,146 @@ theories/Init/specif.cmo: theories/Init/datatypes.cmi \
theories/Init/specif.cmi
theories/Init/specif.cmx: theories/Init/datatypes.cmx \
theories/Init/specif.cmi
+theories/Init/tactics.cmo: theories/Init/tactics.cmi
+theories/Init/tactics.cmx: theories/Init/tactics.cmi
theories/Init/wf.cmo: theories/Init/wf.cmi
theories/Init/wf.cmx: theories/Init/wf.cmi
-theories/IntMap/adalloc.cmo: theories/IntMap/addec.cmi \
- theories/IntMap/addr.cmi theories/NArith/binPos.cmi \
- theories/Init/datatypes.cmi theories/IntMap/map.cmi \
- theories/Init/specif.cmi theories/Bool/sumbool.cmi \
- theories/IntMap/adalloc.cmi
-theories/IntMap/adalloc.cmx: theories/IntMap/addec.cmx \
- theories/IntMap/addr.cmx theories/NArith/binPos.cmx \
- theories/Init/datatypes.cmx theories/IntMap/map.cmx \
- theories/Init/specif.cmx theories/Bool/sumbool.cmx \
- theories/IntMap/adalloc.cmi
-theories/IntMap/addec.cmo: theories/IntMap/addr.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
- theories/Init/specif.cmi theories/Bool/sumbool.cmi \
- theories/IntMap/addec.cmi
-theories/IntMap/addec.cmx: theories/IntMap/addr.cmx \
- theories/NArith/binPos.cmx theories/Init/datatypes.cmx \
- theories/Init/specif.cmx theories/Bool/sumbool.cmx \
- theories/IntMap/addec.cmi
-theories/IntMap/addr.cmo: theories/NArith/binPos.cmi theories/Bool/bool.cmi \
- theories/Init/datatypes.cmi theories/Init/specif.cmi \
- theories/IntMap/addr.cmi
-theories/IntMap/addr.cmx: theories/NArith/binPos.cmx theories/Bool/bool.cmx \
- theories/Init/datatypes.cmx theories/Init/specif.cmx \
- theories/IntMap/addr.cmi
-theories/IntMap/adist.cmo: theories/IntMap/addr.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
- theories/IntMap/adist.cmi
-theories/IntMap/adist.cmx: theories/IntMap/addr.cmx \
- theories/NArith/binPos.cmx theories/Init/datatypes.cmx \
- theories/IntMap/adist.cmi
+theories/IntMap/adalloc.cmo: theories/Bool/sumbool.cmi \
+ theories/Init/specif.cmi theories/NArith/ndec.cmi theories/IntMap/map.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/NArith/binNat.cmi theories/IntMap/adalloc.cmi
+theories/IntMap/adalloc.cmx: theories/Bool/sumbool.cmx \
+ theories/Init/specif.cmx theories/NArith/ndec.cmx theories/IntMap/map.cmx \
+ theories/Init/datatypes.cmx theories/NArith/binPos.cmx \
+ theories/NArith/binNat.cmx theories/IntMap/adalloc.cmi
theories/IntMap/allmaps.cmo: theories/IntMap/allmaps.cmi
theories/IntMap/allmaps.cmx: theories/IntMap/allmaps.cmi
-theories/IntMap/fset.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
- theories/Init/datatypes.cmi theories/IntMap/map.cmi \
- theories/Init/specif.cmi theories/IntMap/fset.cmi
-theories/IntMap/fset.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \
- theories/Init/datatypes.cmx theories/IntMap/map.cmx \
- theories/Init/specif.cmx theories/IntMap/fset.cmi
-theories/IntMap/lsort.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
- theories/NArith/binPos.cmi theories/Bool/bool.cmi \
- theories/Init/datatypes.cmi theories/Lists/list.cmi \
- theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \
- theories/Init/specif.cmi theories/Bool/sumbool.cmi \
- theories/IntMap/lsort.cmi
-theories/IntMap/lsort.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \
- theories/NArith/binPos.cmx theories/Bool/bool.cmx \
- theories/Init/datatypes.cmx theories/Lists/list.cmx \
- theories/IntMap/map.cmx theories/IntMap/mapiter.cmx \
- theories/Init/specif.cmx theories/Bool/sumbool.cmx \
- theories/IntMap/lsort.cmi
+theories/IntMap/fset.cmo: theories/Init/specif.cmi \
+ theories/NArith/ndigits.cmi theories/NArith/ndec.cmi \
+ theories/IntMap/map.cmi theories/Init/datatypes.cmi \
+ theories/NArith/binNat.cmi theories/IntMap/fset.cmi
+theories/IntMap/fset.cmx: theories/Init/specif.cmx \
+ theories/NArith/ndigits.cmx theories/NArith/ndec.cmx \
+ theories/IntMap/map.cmx theories/Init/datatypes.cmx \
+ theories/NArith/binNat.cmx theories/IntMap/fset.cmi
+theories/IntMap/lsort.cmo: theories/Bool/sumbool.cmi theories/Init/specif.cmi \
+ theories/NArith/ndigits.cmi theories/NArith/ndec.cmi \
+ theories/IntMap/mapiter.cmi theories/IntMap/map.cmi \
+ theories/Lists/list.cmi theories/Init/datatypes.cmi \
+ theories/NArith/binNat.cmi theories/IntMap/lsort.cmi
+theories/IntMap/lsort.cmx: theories/Bool/sumbool.cmx theories/Init/specif.cmx \
+ theories/NArith/ndigits.cmx theories/NArith/ndec.cmx \
+ theories/IntMap/mapiter.cmx theories/IntMap/map.cmx \
+ theories/Lists/list.cmx theories/Init/datatypes.cmx \
+ theories/NArith/binNat.cmx theories/IntMap/lsort.cmi
theories/IntMap/mapaxioms.cmo: theories/IntMap/mapaxioms.cmi
theories/IntMap/mapaxioms.cmx: theories/IntMap/mapaxioms.cmi
-theories/IntMap/mapcanon.cmo: theories/IntMap/map.cmi \
- theories/Init/specif.cmi theories/IntMap/mapcanon.cmi
-theories/IntMap/mapcanon.cmx: theories/IntMap/map.cmx \
- theories/Init/specif.cmx theories/IntMap/mapcanon.cmi
-theories/IntMap/mapcard.cmo: theories/IntMap/addec.cmi \
- theories/IntMap/addr.cmi theories/Init/datatypes.cmi \
- theories/IntMap/map.cmi theories/Init/peano.cmi \
- theories/Arith/peano_dec.cmi theories/Arith/plus.cmi \
- theories/Init/specif.cmi theories/Bool/sumbool.cmi \
- theories/IntMap/mapcard.cmi
-theories/IntMap/mapcard.cmx: theories/IntMap/addec.cmx \
- theories/IntMap/addr.cmx theories/Init/datatypes.cmx \
- theories/IntMap/map.cmx theories/Init/peano.cmx \
- theories/Arith/peano_dec.cmx theories/Arith/plus.cmx \
- theories/Init/specif.cmx theories/Bool/sumbool.cmx \
- theories/IntMap/mapcard.cmi
+theories/IntMap/mapcanon.cmo: theories/Init/specif.cmi \
+ theories/IntMap/map.cmi theories/IntMap/mapcanon.cmi
+theories/IntMap/mapcanon.cmx: theories/Init/specif.cmx \
+ theories/IntMap/map.cmx theories/IntMap/mapcanon.cmi
+theories/IntMap/mapcard.cmo: theories/Bool/sumbool.cmi \
+ theories/Init/specif.cmi theories/Arith/plus.cmi \
+ theories/Arith/peano_dec.cmi theories/Init/peano.cmi \
+ theories/NArith/ndigits.cmi theories/NArith/ndec.cmi \
+ theories/IntMap/map.cmi theories/Init/datatypes.cmi \
+ theories/NArith/binNat.cmi theories/IntMap/mapcard.cmi
+theories/IntMap/mapcard.cmx: theories/Bool/sumbool.cmx \
+ theories/Init/specif.cmx theories/Arith/plus.cmx \
+ theories/Arith/peano_dec.cmx theories/Init/peano.cmx \
+ theories/NArith/ndigits.cmx theories/NArith/ndec.cmx \
+ theories/IntMap/map.cmx theories/Init/datatypes.cmx \
+ theories/NArith/binNat.cmx theories/IntMap/mapcard.cmi
theories/IntMap/mapc.cmo: theories/IntMap/mapc.cmi
theories/IntMap/mapc.cmx: theories/IntMap/mapc.cmi
-theories/IntMap/mapfold.cmo: theories/IntMap/addr.cmi \
- theories/Init/datatypes.cmi theories/IntMap/fset.cmi \
- theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \
- theories/Init/specif.cmi theories/IntMap/mapfold.cmi
-theories/IntMap/mapfold.cmx: theories/IntMap/addr.cmx \
- theories/Init/datatypes.cmx theories/IntMap/fset.cmx \
- theories/IntMap/map.cmx theories/IntMap/mapiter.cmx \
- theories/Init/specif.cmx theories/IntMap/mapfold.cmi
-theories/IntMap/mapiter.cmo: theories/IntMap/addec.cmi \
- theories/IntMap/addr.cmi theories/Init/datatypes.cmi \
- theories/Lists/list.cmi theories/IntMap/map.cmi theories/Init/specif.cmi \
- theories/Bool/sumbool.cmi theories/IntMap/mapiter.cmi
-theories/IntMap/mapiter.cmx: theories/IntMap/addec.cmx \
- theories/IntMap/addr.cmx theories/Init/datatypes.cmx \
- theories/Lists/list.cmx theories/IntMap/map.cmx theories/Init/specif.cmx \
- theories/Bool/sumbool.cmx theories/IntMap/mapiter.cmi
-theories/IntMap/maplists.cmo: theories/IntMap/addec.cmi \
- theories/IntMap/addr.cmi theories/Init/datatypes.cmi \
- theories/IntMap/fset.cmi theories/Lists/list.cmi theories/IntMap/map.cmi \
- theories/IntMap/mapiter.cmi theories/Init/specif.cmi \
- theories/Bool/sumbool.cmi theories/IntMap/maplists.cmi
-theories/IntMap/maplists.cmx: theories/IntMap/addec.cmx \
- theories/IntMap/addr.cmx theories/Init/datatypes.cmx \
- theories/IntMap/fset.cmx theories/Lists/list.cmx theories/IntMap/map.cmx \
- theories/IntMap/mapiter.cmx theories/Init/specif.cmx \
- theories/Bool/sumbool.cmx theories/IntMap/maplists.cmi
-theories/IntMap/map.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
- theories/Init/peano.cmi theories/Init/specif.cmi theories/IntMap/map.cmi
-theories/IntMap/map.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \
- theories/NArith/binPos.cmx theories/Init/datatypes.cmx \
- theories/Init/peano.cmx theories/Init/specif.cmx theories/IntMap/map.cmi
-theories/IntMap/mapsubset.cmo: theories/Bool/bool.cmi \
- theories/Init/datatypes.cmi theories/IntMap/fset.cmi \
- theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \
+theories/IntMap/mapfold.cmo: theories/Init/specif.cmi \
+ theories/IntMap/mapiter.cmi theories/IntMap/map.cmi \
+ theories/IntMap/fset.cmi theories/Init/datatypes.cmi \
+ theories/IntMap/mapfold.cmi
+theories/IntMap/mapfold.cmx: theories/Init/specif.cmx \
+ theories/IntMap/mapiter.cmx theories/IntMap/map.cmx \
+ theories/IntMap/fset.cmx theories/Init/datatypes.cmx \
+ theories/IntMap/mapfold.cmi
+theories/IntMap/mapiter.cmo: theories/Bool/sumbool.cmi \
+ theories/Init/specif.cmi theories/NArith/ndigits.cmi \
+ theories/NArith/ndec.cmi theories/IntMap/map.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binNat.cmi \
+ theories/IntMap/mapiter.cmi
+theories/IntMap/mapiter.cmx: theories/Bool/sumbool.cmx \
+ theories/Init/specif.cmx theories/NArith/ndigits.cmx \
+ theories/NArith/ndec.cmx theories/IntMap/map.cmx theories/Lists/list.cmx \
+ theories/Init/datatypes.cmx theories/NArith/binNat.cmx \
+ theories/IntMap/mapiter.cmi
+theories/IntMap/maplists.cmo: theories/Bool/sumbool.cmi \
+ theories/Init/specif.cmi theories/NArith/ndec.cmi \
+ theories/IntMap/mapiter.cmi theories/IntMap/map.cmi \
+ theories/Lists/list.cmi theories/IntMap/fset.cmi \
+ theories/Init/datatypes.cmi theories/IntMap/maplists.cmi
+theories/IntMap/maplists.cmx: theories/Bool/sumbool.cmx \
+ theories/Init/specif.cmx theories/NArith/ndec.cmx \
+ theories/IntMap/mapiter.cmx theories/IntMap/map.cmx \
+ theories/Lists/list.cmx theories/IntMap/fset.cmx \
+ theories/Init/datatypes.cmx theories/IntMap/maplists.cmi
+theories/IntMap/map.cmo: theories/Init/specif.cmi theories/Init/peano.cmi \
+ theories/NArith/ndigits.cmi theories/NArith/ndec.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/NArith/binNat.cmi theories/IntMap/map.cmi
+theories/IntMap/map.cmx: theories/Init/specif.cmx theories/Init/peano.cmx \
+ theories/NArith/ndigits.cmx theories/NArith/ndec.cmx \
+ theories/Init/datatypes.cmx theories/NArith/binPos.cmx \
+ theories/NArith/binNat.cmx theories/IntMap/map.cmi
+theories/IntMap/mapsubset.cmo: theories/IntMap/mapiter.cmi \
+ theories/IntMap/map.cmi theories/IntMap/fset.cmi \
+ theories/Init/datatypes.cmi theories/Bool/bool.cmi \
theories/IntMap/mapsubset.cmi
-theories/IntMap/mapsubset.cmx: theories/Bool/bool.cmx \
- theories/Init/datatypes.cmx theories/IntMap/fset.cmx \
- theories/IntMap/map.cmx theories/IntMap/mapiter.cmx \
+theories/IntMap/mapsubset.cmx: theories/IntMap/mapiter.cmx \
+ theories/IntMap/map.cmx theories/IntMap/fset.cmx \
+ theories/Init/datatypes.cmx theories/Bool/bool.cmx \
theories/IntMap/mapsubset.cmi
-theories/Lists/list.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \
+theories/Lists/list.cmo: theories/Init/specif.cmi theories/Init/datatypes.cmi \
theories/Lists/list.cmi
-theories/Lists/list.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \
+theories/Lists/list.cmx: theories/Init/specif.cmx theories/Init/datatypes.cmx \
theories/Lists/list.cmi
-theories/Lists/listSet.cmo: theories/Init/datatypes.cmi \
- theories/Lists/list.cmi theories/Init/specif.cmi \
- theories/Lists/listSet.cmi
-theories/Lists/listSet.cmx: theories/Init/datatypes.cmx \
- theories/Lists/list.cmx theories/Init/specif.cmx \
- theories/Lists/listSet.cmi
+theories/Lists/listSet.cmo: theories/Init/specif.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi theories/Lists/listSet.cmi
+theories/Lists/listSet.cmx: theories/Init/specif.cmx theories/Lists/list.cmx \
+ theories/Init/datatypes.cmx theories/Lists/listSet.cmi
theories/Lists/monoList.cmo: theories/Init/datatypes.cmi \
theories/Lists/monoList.cmi
theories/Lists/monoList.cmx: theories/Init/datatypes.cmx \
theories/Lists/monoList.cmi
+theories/Lists/setoidList.cmo: theories/Init/specif.cmi \
+ theories/Lists/list.cmi theories/Init/datatypes.cmi \
+ theories/Lists/setoidList.cmi
+theories/Lists/setoidList.cmx: theories/Init/specif.cmx \
+ theories/Lists/list.cmx theories/Init/datatypes.cmx \
+ theories/Lists/setoidList.cmi
theories/Lists/streams.cmo: theories/Init/datatypes.cmi \
theories/Lists/streams.cmi
theories/Lists/streams.cmx: theories/Init/datatypes.cmx \
theories/Lists/streams.cmi
-theories/Lists/theoryList.cmo: theories/Init/datatypes.cmi \
- theories/Lists/list.cmi theories/Init/specif.cmi \
+theories/Lists/theoryList.cmo: theories/Init/specif.cmi \
+ theories/Lists/list.cmi theories/Init/datatypes.cmi \
theories/Lists/theoryList.cmi
-theories/Lists/theoryList.cmx: theories/Init/datatypes.cmx \
- theories/Lists/list.cmx theories/Init/specif.cmx \
+theories/Lists/theoryList.cmx: theories/Init/specif.cmx \
+ theories/Lists/list.cmx theories/Init/datatypes.cmx \
theories/Lists/theoryList.cmi
theories/Logic/berardi.cmo: theories/Logic/berardi.cmi
theories/Logic/berardi.cmx: theories/Logic/berardi.cmi
-theories/Logic/choiceFacts.cmo: theories/Logic/choiceFacts.cmi
-theories/Logic/choiceFacts.cmx: theories/Logic/choiceFacts.cmi
+theories/Logic/choiceFacts.cmo: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/Logic/choiceFacts.cmi
+theories/Logic/choiceFacts.cmx: theories/Init/specif.cmx \
+ theories/Init/datatypes.cmx theories/Logic/choiceFacts.cmi
theories/Logic/classicalChoice.cmo: theories/Logic/classicalChoice.cmi
theories/Logic/classicalChoice.cmx: theories/Logic/classicalChoice.cmi
-theories/Logic/classicalDescription.cmo: \
- theories/Logic/classicalDescription.cmi
-theories/Logic/classicalDescription.cmx: \
- theories/Logic/classicalDescription.cmi
+theories/Logic/classicalDescription.cmo: theories/Init/specif.cmi \
+ theories/Logic/choiceFacts.cmi theories/Logic/classicalDescription.cmi
+theories/Logic/classicalDescription.cmx: theories/Init/specif.cmx \
+ theories/Logic/choiceFacts.cmx theories/Logic/classicalDescription.cmi
+theories/Logic/classicalEpsilon.cmo: theories/Init/specif.cmi \
+ theories/Logic/choiceFacts.cmi theories/Logic/classicalEpsilon.cmi
+theories/Logic/classicalEpsilon.cmx: theories/Init/specif.cmx \
+ theories/Logic/choiceFacts.cmx theories/Logic/classicalEpsilon.cmi
theories/Logic/classicalFacts.cmo: theories/Logic/classicalFacts.cmi
theories/Logic/classicalFacts.cmx: theories/Logic/classicalFacts.cmi
theories/Logic/classical.cmo: theories/Logic/classical.cmi
@@ -272,38 +474,118 @@ theories/Logic/classical_Pred_Type.cmo: \
theories/Logic/classical_Pred_Type.cmi
theories/Logic/classical_Pred_Type.cmx: \
theories/Logic/classical_Pred_Type.cmi
-theories/Logic/classical_Prop.cmo: theories/Logic/classical_Prop.cmi
-theories/Logic/classical_Prop.cmx: theories/Logic/classical_Prop.cmi
+theories/Logic/classical_Prop.cmo: theories/Logic/eqdepFacts.cmi \
+ theories/Logic/classical_Prop.cmi
+theories/Logic/classical_Prop.cmx: theories/Logic/eqdepFacts.cmx \
+ theories/Logic/classical_Prop.cmi
theories/Logic/classical_Type.cmo: theories/Logic/classical_Type.cmi
theories/Logic/classical_Type.cmx: theories/Logic/classical_Type.cmi
+theories/Logic/classicalUniqueChoice.cmo: \
+ theories/Logic/classicalUniqueChoice.cmi
+theories/Logic/classicalUniqueChoice.cmx: \
+ theories/Logic/classicalUniqueChoice.cmi
theories/Logic/decidable.cmo: theories/Logic/decidable.cmi
theories/Logic/decidable.cmx: theories/Logic/decidable.cmi
-theories/Logic/diaconescu.cmo: theories/Logic/diaconescu.cmi
-theories/Logic/diaconescu.cmx: theories/Logic/diaconescu.cmi
-theories/Logic/eqdep_dec.cmo: theories/Logic/eqdep_dec.cmi
-theories/Logic/eqdep_dec.cmx: theories/Logic/eqdep_dec.cmi
-theories/Logic/eqdep.cmo: theories/Logic/eqdep.cmi
-theories/Logic/eqdep.cmx: theories/Logic/eqdep.cmi
+theories/Logic/diaconescu.cmo: theories/Init/specif.cmi \
+ theories/Logic/diaconescu.cmi
+theories/Logic/diaconescu.cmx: theories/Init/specif.cmx \
+ theories/Logic/diaconescu.cmi
+theories/Logic/eqdep_dec.cmo: theories/Init/specif.cmi \
+ theories/Logic/eqdep_dec.cmi
+theories/Logic/eqdep_dec.cmx: theories/Init/specif.cmx \
+ theories/Logic/eqdep_dec.cmi
+theories/Logic/eqdepFacts.cmo: theories/Logic/eqdepFacts.cmi
+theories/Logic/eqdepFacts.cmx: theories/Logic/eqdepFacts.cmi
+theories/Logic/eqdep.cmo: theories/Logic/eqdepFacts.cmi \
+ theories/Logic/eqdep.cmi
+theories/Logic/eqdep.cmx: theories/Logic/eqdepFacts.cmx \
+ theories/Logic/eqdep.cmi
theories/Logic/hurkens.cmo: theories/Logic/hurkens.cmi
theories/Logic/hurkens.cmx: theories/Logic/hurkens.cmi
theories/Logic/jMeq.cmo: theories/Logic/jMeq.cmi
theories/Logic/jMeq.cmx: theories/Logic/jMeq.cmi
-theories/Logic/proofIrrelevance.cmo: theories/Logic/proofIrrelevance.cmi
-theories/Logic/proofIrrelevance.cmx: theories/Logic/proofIrrelevance.cmi
+theories/Logic/proofIrrelevanceFacts.cmo: theories/Logic/eqdepFacts.cmi \
+ theories/Logic/proofIrrelevanceFacts.cmi
+theories/Logic/proofIrrelevanceFacts.cmx: theories/Logic/eqdepFacts.cmx \
+ theories/Logic/proofIrrelevanceFacts.cmi
+theories/Logic/proofIrrelevance.cmo: theories/Logic/proofIrrelevanceFacts.cmi \
+ theories/Logic/proofIrrelevance.cmi
+theories/Logic/proofIrrelevance.cmx: theories/Logic/proofIrrelevanceFacts.cmx \
+ theories/Logic/proofIrrelevance.cmi
theories/Logic/relationalChoice.cmo: theories/Logic/relationalChoice.cmi
theories/Logic/relationalChoice.cmx: theories/Logic/relationalChoice.cmi
-theories/NArith/binNat.cmo: theories/NArith/binPos.cmi \
- theories/Init/datatypes.cmi theories/NArith/binNat.cmi
-theories/NArith/binNat.cmx: theories/NArith/binPos.cmx \
- theories/Init/datatypes.cmx theories/NArith/binNat.cmi
-theories/NArith/binPos.cmo: theories/Init/datatypes.cmi \
- theories/Init/peano.cmi theories/NArith/binPos.cmi
-theories/NArith/binPos.cmx: theories/Init/datatypes.cmx \
- theories/Init/peano.cmx theories/NArith/binPos.cmi
+theories/NArith/binNat.cmo: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/NArith/binNat.cmi
+theories/NArith/binNat.cmx: theories/Init/specif.cmx \
+ theories/Init/datatypes.cmx theories/NArith/binPos.cmx \
+ theories/NArith/binNat.cmi
+theories/NArith/binPos.cmo: theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi
+theories/NArith/binPos.cmx: theories/Init/peano.cmx \
+ theories/Init/datatypes.cmx theories/NArith/binPos.cmi
theories/NArith/nArith.cmo: theories/NArith/nArith.cmi
theories/NArith/nArith.cmx: theories/NArith/nArith.cmi
+theories/NArith/ndec.cmo: theories/Bool/sumbool.cmi theories/Init/specif.cmi \
+ theories/NArith/nnat.cmi theories/NArith/ndigits.cmi \
+ theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi \
+ theories/NArith/binPos.cmi theories/NArith/binNat.cmi \
+ theories/NArith/ndec.cmi
+theories/NArith/ndec.cmx: theories/Bool/sumbool.cmx theories/Init/specif.cmx \
+ theories/NArith/nnat.cmx theories/NArith/ndigits.cmx \
+ theories/Init/datatypes.cmx theories/Arith/compare_dec.cmx \
+ theories/NArith/binPos.cmx theories/NArith/binNat.cmx \
+ theories/NArith/ndec.cmi
+theories/NArith/ndigits.cmo: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/Bool/bvector.cmi \
+ theories/Bool/bool.cmi theories/NArith/binPos.cmi \
+ theories/NArith/binNat.cmi theories/NArith/ndigits.cmi
+theories/NArith/ndigits.cmx: theories/Init/specif.cmx \
+ theories/Init/datatypes.cmx theories/Bool/bvector.cmx \
+ theories/Bool/bool.cmx theories/NArith/binPos.cmx \
+ theories/NArith/binNat.cmx theories/NArith/ndigits.cmi
+theories/NArith/ndist.cmo: theories/NArith/ndigits.cmi theories/Arith/min.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/NArith/binNat.cmi theories/NArith/ndist.cmi
+theories/NArith/ndist.cmx: theories/NArith/ndigits.cmx theories/Arith/min.cmx \
+ theories/Init/datatypes.cmx theories/NArith/binPos.cmx \
+ theories/NArith/binNat.cmx theories/NArith/ndist.cmi
+theories/NArith/nnat.cmo: theories/Init/datatypes.cmi \
+ theories/NArith/binPos.cmi theories/NArith/binNat.cmi \
+ theories/NArith/nnat.cmi
+theories/NArith/nnat.cmx: theories/Init/datatypes.cmx \
+ theories/NArith/binPos.cmx theories/NArith/binNat.cmx \
+ theories/NArith/nnat.cmi
theories/NArith/pnat.cmo: theories/NArith/pnat.cmi
theories/NArith/pnat.cmx: theories/NArith/pnat.cmi
+theories/QArith/qArith_base.cmo: theories/ZArith/zArith_dec.cmi \
+ theories/Init/specif.cmi theories/Setoids/setoid.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi theories/QArith/qArith_base.cmi
+theories/QArith/qArith_base.cmx: theories/ZArith/zArith_dec.cmx \
+ theories/Init/specif.cmx theories/Setoids/setoid.cmx \
+ theories/Init/datatypes.cmx theories/NArith/binPos.cmx \
+ theories/ZArith/binInt.cmx theories/QArith/qArith_base.cmi
+theories/QArith/qArith.cmo: theories/QArith/qArith.cmi
+theories/QArith/qArith.cmx: theories/QArith/qArith.cmi
+theories/QArith/qreals.cmo: theories/QArith/qArith_base.cmi \
+ theories/ZArith/binInt.cmi theories/QArith/qreals.cmi
+theories/QArith/qreals.cmx: theories/QArith/qArith_base.cmx \
+ theories/ZArith/binInt.cmx theories/QArith/qreals.cmi
+theories/QArith/qreduction.cmo: theories/ZArith/znumtheory.cmi \
+ theories/Setoids/setoid.cmi theories/QArith/qArith_base.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi theories/QArith/qreduction.cmi
+theories/QArith/qreduction.cmx: theories/ZArith/znumtheory.cmx \
+ theories/Setoids/setoid.cmx theories/QArith/qArith_base.cmx \
+ theories/Init/datatypes.cmx theories/NArith/binPos.cmx \
+ theories/ZArith/binInt.cmx theories/QArith/qreduction.cmi
+theories/QArith/qring.cmo: theories/Init/specif.cmi \
+ theories/QArith/qArith_base.cmi theories/Init/datatypes.cmi \
+ theories/QArith/qring.cmi
+theories/QArith/qring.cmx: theories/Init/specif.cmx \
+ theories/QArith/qArith_base.cmx theories/Init/datatypes.cmx \
+ theories/QArith/qring.cmi
theories/Relations/newman.cmo: theories/Relations/newman.cmi
theories/Relations/newman.cmx: theories/Relations/newman.cmi
theories/Relations/operators_Properties.cmo: \
@@ -314,16 +596,18 @@ theories/Relations/relation_Definitions.cmo: \
theories/Relations/relation_Definitions.cmi
theories/Relations/relation_Definitions.cmx: \
theories/Relations/relation_Definitions.cmi
-theories/Relations/relation_Operators.cmo: theories/Lists/list.cmi \
- theories/Init/specif.cmi theories/Relations/relation_Operators.cmi
-theories/Relations/relation_Operators.cmx: theories/Lists/list.cmx \
- theories/Init/specif.cmx theories/Relations/relation_Operators.cmi
+theories/Relations/relation_Operators.cmo: theories/Init/specif.cmi \
+ theories/Lists/list.cmi theories/Relations/relation_Operators.cmi
+theories/Relations/relation_Operators.cmx: theories/Init/specif.cmx \
+ theories/Lists/list.cmx theories/Relations/relation_Operators.cmi
theories/Relations/relations.cmo: theories/Relations/relations.cmi
theories/Relations/relations.cmx: theories/Relations/relations.cmi
theories/Relations/rstar.cmo: theories/Relations/rstar.cmi
theories/Relations/rstar.cmx: theories/Relations/rstar.cmi
-theories/Setoids/setoid.cmo: theories/Setoids/setoid.cmi
-theories/Setoids/setoid.cmx: theories/Setoids/setoid.cmi
+theories/Setoids/setoid.cmo: theories/Init/datatypes.cmi \
+ theories/Setoids/setoid.cmi
+theories/Setoids/setoid.cmx: theories/Init/datatypes.cmx \
+ theories/Setoids/setoid.cmi
theories/Sets/classical_sets.cmo: theories/Sets/classical_sets.cmi
theories/Sets/classical_sets.cmx: theories/Sets/classical_sets.cmi
theories/Sets/constructive_sets.cmo: theories/Sets/constructive_sets.cmi
@@ -340,20 +624,18 @@ theories/Sets/image.cmo: theories/Sets/image.cmi
theories/Sets/image.cmx: theories/Sets/image.cmi
theories/Sets/infinite_sets.cmo: theories/Sets/infinite_sets.cmi
theories/Sets/infinite_sets.cmx: theories/Sets/infinite_sets.cmi
-theories/Sets/integers.cmo: theories/Init/datatypes.cmi \
- theories/Sets/partial_Order.cmi theories/Sets/integers.cmi
-theories/Sets/integers.cmx: theories/Init/datatypes.cmx \
- theories/Sets/partial_Order.cmx theories/Sets/integers.cmi
-theories/Sets/multiset.cmo: theories/Init/datatypes.cmi \
- theories/Init/peano.cmi theories/Init/specif.cmi \
- theories/Sets/multiset.cmi
-theories/Sets/multiset.cmx: theories/Init/datatypes.cmx \
- theories/Init/peano.cmx theories/Init/specif.cmx \
- theories/Sets/multiset.cmi
-theories/Sets/partial_Order.cmo: theories/Sets/ensembles.cmi \
- theories/Sets/relations_1.cmi theories/Sets/partial_Order.cmi
-theories/Sets/partial_Order.cmx: theories/Sets/ensembles.cmx \
- theories/Sets/relations_1.cmx theories/Sets/partial_Order.cmi
+theories/Sets/integers.cmo: theories/Sets/partial_Order.cmi \
+ theories/Init/datatypes.cmi theories/Sets/integers.cmi
+theories/Sets/integers.cmx: theories/Sets/partial_Order.cmx \
+ theories/Init/datatypes.cmx theories/Sets/integers.cmi
+theories/Sets/multiset.cmo: theories/Init/specif.cmi theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi theories/Sets/multiset.cmi
+theories/Sets/multiset.cmx: theories/Init/specif.cmx theories/Init/peano.cmx \
+ theories/Init/datatypes.cmx theories/Sets/multiset.cmi
+theories/Sets/partial_Order.cmo: theories/Sets/relations_1.cmi \
+ theories/Sets/ensembles.cmi theories/Sets/partial_Order.cmi
+theories/Sets/partial_Order.cmx: theories/Sets/relations_1.cmx \
+ theories/Sets/ensembles.cmx theories/Sets/partial_Order.cmi
theories/Sets/permut.cmo: theories/Sets/permut.cmi
theories/Sets/permut.cmx: theories/Sets/permut.cmi
theories/Sets/powerset_Classical_facts.cmo: \
@@ -362,10 +644,10 @@ theories/Sets/powerset_Classical_facts.cmx: \
theories/Sets/powerset_Classical_facts.cmi
theories/Sets/powerset_facts.cmo: theories/Sets/powerset_facts.cmi
theories/Sets/powerset_facts.cmx: theories/Sets/powerset_facts.cmi
-theories/Sets/powerset.cmo: theories/Sets/ensembles.cmi \
- theories/Sets/partial_Order.cmi theories/Sets/powerset.cmi
-theories/Sets/powerset.cmx: theories/Sets/ensembles.cmx \
- theories/Sets/partial_Order.cmx theories/Sets/powerset.cmi
+theories/Sets/powerset.cmo: theories/Sets/partial_Order.cmi \
+ theories/Sets/ensembles.cmi theories/Sets/powerset.cmi
+theories/Sets/powerset.cmx: theories/Sets/partial_Order.cmx \
+ theories/Sets/ensembles.cmx theories/Sets/powerset.cmi
theories/Sets/relations_1_facts.cmo: theories/Sets/relations_1_facts.cmi
theories/Sets/relations_1_facts.cmx: theories/Sets/relations_1_facts.cmi
theories/Sets/relations_1.cmo: theories/Sets/relations_1.cmi
@@ -378,30 +660,46 @@ theories/Sets/relations_3_facts.cmo: theories/Sets/relations_3_facts.cmi
theories/Sets/relations_3_facts.cmx: theories/Sets/relations_3_facts.cmi
theories/Sets/relations_3.cmo: theories/Sets/relations_3.cmi
theories/Sets/relations_3.cmx: theories/Sets/relations_3.cmi
-theories/Sets/uniset.cmo: theories/Init/datatypes.cmi \
- theories/Init/specif.cmi theories/Sets/uniset.cmi
-theories/Sets/uniset.cmx: theories/Init/datatypes.cmx \
- theories/Init/specif.cmx theories/Sets/uniset.cmi
-theories/Sorting/heap.cmo: theories/Init/datatypes.cmi \
- theories/Lists/list.cmi theories/Sets/multiset.cmi \
- theories/Init/peano.cmi theories/Sorting/sorting.cmi \
- theories/Init/specif.cmi theories/Sorting/heap.cmi
-theories/Sorting/heap.cmx: theories/Init/datatypes.cmx \
- theories/Lists/list.cmx theories/Sets/multiset.cmx \
- theories/Init/peano.cmx theories/Sorting/sorting.cmx \
- theories/Init/specif.cmx theories/Sorting/heap.cmi
-theories/Sorting/permutation.cmo: theories/Init/datatypes.cmi \
- theories/Lists/list.cmi theories/Sets/multiset.cmi \
- theories/Init/peano.cmi theories/Init/specif.cmi \
+theories/Sets/uniset.cmo: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/Sets/uniset.cmi
+theories/Sets/uniset.cmx: theories/Init/specif.cmx \
+ theories/Init/datatypes.cmx theories/Sets/uniset.cmi
+theories/Sorting/heap.cmo: theories/Init/specif.cmi \
+ theories/Sorting/sorting.cmi theories/Init/peano.cmi \
+ theories/Sets/multiset.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi theories/Sorting/heap.cmi
+theories/Sorting/heap.cmx: theories/Init/specif.cmx \
+ theories/Sorting/sorting.cmx theories/Init/peano.cmx \
+ theories/Sets/multiset.cmx theories/Lists/list.cmx \
+ theories/Init/datatypes.cmx theories/Sorting/heap.cmi
+theories/Sorting/permutation.cmo: theories/Init/specif.cmi \
+ theories/Init/peano.cmi theories/Sets/multiset.cmi \
+ theories/Lists/list.cmi theories/Init/datatypes.cmi \
theories/Sorting/permutation.cmi
-theories/Sorting/permutation.cmx: theories/Init/datatypes.cmx \
- theories/Lists/list.cmx theories/Sets/multiset.cmx \
- theories/Init/peano.cmx theories/Init/specif.cmx \
+theories/Sorting/permutation.cmx: theories/Init/specif.cmx \
+ theories/Init/peano.cmx theories/Sets/multiset.cmx \
+ theories/Lists/list.cmx theories/Init/datatypes.cmx \
theories/Sorting/permutation.cmi
-theories/Sorting/sorting.cmo: theories/Lists/list.cmi \
- theories/Init/specif.cmi theories/Sorting/sorting.cmi
-theories/Sorting/sorting.cmx: theories/Lists/list.cmx \
- theories/Init/specif.cmx theories/Sorting/sorting.cmi
+theories/Sorting/permutEq.cmo: theories/Sorting/permutEq.cmi
+theories/Sorting/permutEq.cmx: theories/Sorting/permutEq.cmi
+theories/Sorting/permutSetoid.cmo: theories/Sorting/permutSetoid.cmi
+theories/Sorting/permutSetoid.cmx: theories/Sorting/permutSetoid.cmi
+theories/Sorting/sorting.cmo: theories/Init/specif.cmi \
+ theories/Lists/list.cmi theories/Sorting/sorting.cmi
+theories/Sorting/sorting.cmx: theories/Init/specif.cmx \
+ theories/Lists/list.cmx theories/Sorting/sorting.cmi
+theories/Strings/ascii.cmo: theories/Init/specif.cmi theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi theories/Bool/bool.cmi \
+ theories/NArith/binPos.cmi theories/Strings/ascii.cmi
+theories/Strings/ascii.cmx: theories/Init/specif.cmx theories/Init/peano.cmx \
+ theories/Init/datatypes.cmx theories/Bool/bool.cmx \
+ theories/NArith/binPos.cmx theories/Strings/ascii.cmi
+theories/Strings/string.cmo: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/Strings/ascii.cmi \
+ theories/Strings/string.cmi
+theories/Strings/string.cmx: theories/Init/specif.cmx \
+ theories/Init/datatypes.cmx theories/Strings/ascii.cmx \
+ theories/Strings/string.cmi
theories/Wellfounded/disjoint_Union.cmo: \
theories/Wellfounded/disjoint_Union.cmi
theories/Wellfounded/disjoint_Union.cmx: \
@@ -434,280 +732,405 @@ theories/Wellfounded/well_Ordering.cmx: theories/Init/specif.cmx \
theories/Wellfounded/well_Ordering.cmi
theories/ZArith/auxiliary.cmo: theories/ZArith/auxiliary.cmi
theories/ZArith/auxiliary.cmx: theories/ZArith/auxiliary.cmi
-theories/ZArith/binInt.cmo: theories/NArith/binNat.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
+theories/ZArith/binInt.cmo: theories/Init/datatypes.cmi \
+ theories/NArith/binPos.cmi theories/NArith/binNat.cmi \
theories/ZArith/binInt.cmi
-theories/ZArith/binInt.cmx: theories/NArith/binNat.cmx \
- theories/NArith/binPos.cmx theories/Init/datatypes.cmx \
+theories/ZArith/binInt.cmx: theories/Init/datatypes.cmx \
+ theories/NArith/binPos.cmx theories/NArith/binNat.cmx \
theories/ZArith/binInt.cmi
-theories/ZArith/wf_Z.cmo: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
- theories/Init/peano.cmi theories/Init/specif.cmi theories/ZArith/wf_Z.cmi
-theories/ZArith/wf_Z.cmx: theories/ZArith/binInt.cmx \
- theories/NArith/binPos.cmx theories/Init/datatypes.cmx \
- theories/Init/peano.cmx theories/Init/specif.cmx theories/ZArith/wf_Z.cmi
-theories/ZArith/zabs.cmo: theories/ZArith/binInt.cmi theories/Init/specif.cmi \
- theories/Bool/sumbool.cmi theories/ZArith/zabs.cmi
-theories/ZArith/zabs.cmx: theories/ZArith/binInt.cmx theories/Init/specif.cmx \
- theories/Bool/sumbool.cmx theories/ZArith/zabs.cmi
+theories/ZArith/wf_Z.cmo: theories/Init/specif.cmi theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi theories/ZArith/wf_Z.cmi
+theories/ZArith/wf_Z.cmx: theories/Init/specif.cmx theories/Init/peano.cmx \
+ theories/Init/datatypes.cmx theories/NArith/binPos.cmx \
+ theories/ZArith/binInt.cmx theories/ZArith/wf_Z.cmi
+theories/ZArith/zabs.cmo: theories/Init/specif.cmi theories/ZArith/binInt.cmi \
+ theories/ZArith/zabs.cmi
+theories/ZArith/zabs.cmx: theories/Init/specif.cmx theories/ZArith/binInt.cmx \
+ theories/ZArith/zabs.cmi
theories/ZArith/zArith_base.cmo: theories/ZArith/zArith_base.cmi
theories/ZArith/zArith_base.cmx: theories/ZArith/zArith_base.cmi
-theories/ZArith/zArith_dec.cmo: theories/ZArith/binInt.cmi \
- theories/Init/datatypes.cmi theories/Init/specif.cmi \
- theories/Bool/sumbool.cmi theories/ZArith/zArith_dec.cmi
-theories/ZArith/zArith_dec.cmx: theories/ZArith/binInt.cmx \
- theories/Init/datatypes.cmx theories/Init/specif.cmx \
- theories/Bool/sumbool.cmx theories/ZArith/zArith_dec.cmi
+theories/ZArith/zArith_dec.cmo: theories/Bool/sumbool.cmi \
+ theories/Init/specif.cmi theories/Init/datatypes.cmi \
+ theories/ZArith/binInt.cmi theories/ZArith/zArith_dec.cmi
+theories/ZArith/zArith_dec.cmx: theories/Bool/sumbool.cmx \
+ theories/Init/specif.cmx theories/Init/datatypes.cmx \
+ theories/ZArith/binInt.cmx theories/ZArith/zArith_dec.cmi
theories/ZArith/zArith.cmo: theories/ZArith/zArith.cmi
theories/ZArith/zArith.cmx: theories/ZArith/zArith.cmi
-theories/ZArith/zbinary.cmo: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Bool/bvector.cmi \
- theories/Init/datatypes.cmi theories/ZArith/zeven.cmi \
+theories/ZArith/zbinary.cmo: theories/ZArith/zeven.cmi \
+ theories/Init/datatypes.cmi theories/Bool/bvector.cmi \
+ theories/NArith/binPos.cmi theories/ZArith/binInt.cmi \
theories/ZArith/zbinary.cmi
-theories/ZArith/zbinary.cmx: theories/ZArith/binInt.cmx \
- theories/NArith/binPos.cmx theories/Bool/bvector.cmx \
- theories/Init/datatypes.cmx theories/ZArith/zeven.cmx \
+theories/ZArith/zbinary.cmx: theories/ZArith/zeven.cmx \
+ theories/Init/datatypes.cmx theories/Bool/bvector.cmx \
+ theories/NArith/binPos.cmx theories/ZArith/binInt.cmx \
theories/ZArith/zbinary.cmi
-theories/ZArith/zbool.cmo: theories/ZArith/binInt.cmi \
- theories/Init/datatypes.cmi theories/Init/specif.cmi \
- theories/Bool/sumbool.cmi theories/ZArith/zArith_dec.cmi \
- theories/ZArith/zeven.cmi theories/ZArith/zbool.cmi
-theories/ZArith/zbool.cmx: theories/ZArith/binInt.cmx \
- theories/Init/datatypes.cmx theories/Init/specif.cmx \
- theories/Bool/sumbool.cmx theories/ZArith/zArith_dec.cmx \
- theories/ZArith/zeven.cmx theories/ZArith/zbool.cmi
+theories/ZArith/zbool.cmo: theories/ZArith/zeven.cmi \
+ theories/ZArith/zArith_dec.cmi theories/Bool/sumbool.cmi \
+ theories/Init/specif.cmi theories/Init/datatypes.cmi \
+ theories/ZArith/binInt.cmi theories/ZArith/zbool.cmi
+theories/ZArith/zbool.cmx: theories/ZArith/zeven.cmx \
+ theories/ZArith/zArith_dec.cmx theories/Bool/sumbool.cmx \
+ theories/Init/specif.cmx theories/Init/datatypes.cmx \
+ theories/ZArith/binInt.cmx theories/ZArith/zbool.cmi
theories/ZArith/zcompare.cmo: theories/ZArith/zcompare.cmi
theories/ZArith/zcompare.cmx: theories/ZArith/zcompare.cmi
-theories/ZArith/zcomplements.cmo: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
- theories/Lists/list.cmi theories/Init/specif.cmi theories/ZArith/wf_Z.cmi \
- theories/ZArith/zabs.cmi theories/ZArith/zcomplements.cmi
-theories/ZArith/zcomplements.cmx: theories/ZArith/binInt.cmx \
- theories/NArith/binPos.cmx theories/Init/datatypes.cmx \
- theories/Lists/list.cmx theories/Init/specif.cmx theories/ZArith/wf_Z.cmx \
- theories/ZArith/zabs.cmx theories/ZArith/zcomplements.cmi
-theories/ZArith/zdiv.cmo: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
- theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \
- theories/ZArith/zbool.cmi theories/ZArith/zdiv.cmi
-theories/ZArith/zdiv.cmx: theories/ZArith/binInt.cmx \
- theories/NArith/binPos.cmx theories/Init/datatypes.cmx \
- theories/Init/specif.cmx theories/ZArith/zArith_dec.cmx \
- theories/ZArith/zbool.cmx theories/ZArith/zdiv.cmi
-theories/ZArith/zeven.cmo: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
- theories/Init/specif.cmi theories/ZArith/zeven.cmi
-theories/ZArith/zeven.cmx: theories/ZArith/binInt.cmx \
- theories/NArith/binPos.cmx theories/Init/datatypes.cmx \
- theories/Init/specif.cmx theories/ZArith/zeven.cmi
+theories/ZArith/zcomplements.cmo: theories/ZArith/zabs.cmi \
+ theories/ZArith/wf_Z.cmi theories/Init/specif.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi theories/ZArith/zcomplements.cmi
+theories/ZArith/zcomplements.cmx: theories/ZArith/zabs.cmx \
+ theories/ZArith/wf_Z.cmx theories/Init/specif.cmx theories/Lists/list.cmx \
+ theories/Init/datatypes.cmx theories/NArith/binPos.cmx \
+ theories/ZArith/binInt.cmx theories/ZArith/zcomplements.cmi
+theories/ZArith/zdiv.cmo: theories/ZArith/zbool.cmi \
+ theories/ZArith/zArith_dec.cmi theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi theories/ZArith/zdiv.cmi
+theories/ZArith/zdiv.cmx: theories/ZArith/zbool.cmx \
+ theories/ZArith/zArith_dec.cmx theories/Init/specif.cmx \
+ theories/Init/datatypes.cmx theories/NArith/binPos.cmx \
+ theories/ZArith/binInt.cmx theories/ZArith/zdiv.cmi
+theories/ZArith/zeven.cmo: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi theories/ZArith/zeven.cmi
+theories/ZArith/zeven.cmx: theories/Init/specif.cmx \
+ theories/Init/datatypes.cmx theories/NArith/binPos.cmx \
+ theories/ZArith/binInt.cmx theories/ZArith/zeven.cmi
theories/ZArith/zhints.cmo: theories/ZArith/zhints.cmi
theories/ZArith/zhints.cmx: theories/ZArith/zhints.cmi
-theories/ZArith/zlogarithm.cmo: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/ZArith/zlogarithm.cmi
-theories/ZArith/zlogarithm.cmx: theories/ZArith/binInt.cmx \
- theories/NArith/binPos.cmx theories/ZArith/zlogarithm.cmi
-theories/ZArith/zmin.cmo: theories/ZArith/binInt.cmi \
- theories/Init/datatypes.cmi theories/ZArith/zmin.cmi
-theories/ZArith/zmin.cmx: theories/ZArith/binInt.cmx \
- theories/Init/datatypes.cmx theories/ZArith/zmin.cmi
-theories/ZArith/zmisc.cmo: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
+theories/ZArith/zlogarithm.cmo: theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi theories/ZArith/zlogarithm.cmi
+theories/ZArith/zlogarithm.cmx: theories/NArith/binPos.cmx \
+ theories/ZArith/binInt.cmx theories/ZArith/zlogarithm.cmi
+theories/ZArith/zmax.cmo: theories/Init/datatypes.cmi \
+ theories/ZArith/binInt.cmi theories/ZArith/zmax.cmi
+theories/ZArith/zmax.cmx: theories/Init/datatypes.cmx \
+ theories/ZArith/binInt.cmx theories/ZArith/zmax.cmi
+theories/ZArith/zminmax.cmo: theories/ZArith/zminmax.cmi
+theories/ZArith/zminmax.cmx: theories/ZArith/zminmax.cmi
+theories/ZArith/zmin.cmo: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/ZArith/binInt.cmi \
+ theories/ZArith/zmin.cmi
+theories/ZArith/zmin.cmx: theories/Init/specif.cmx \
+ theories/Init/datatypes.cmx theories/ZArith/binInt.cmx \
+ theories/ZArith/zmin.cmi
+theories/ZArith/zmisc.cmo: theories/Init/datatypes.cmi \
+ theories/NArith/binPos.cmi theories/ZArith/binInt.cmi \
theories/ZArith/zmisc.cmi
-theories/ZArith/zmisc.cmx: theories/ZArith/binInt.cmx \
- theories/NArith/binPos.cmx theories/Init/datatypes.cmx \
+theories/ZArith/zmisc.cmx: theories/Init/datatypes.cmx \
+ theories/NArith/binPos.cmx theories/ZArith/binInt.cmx \
theories/ZArith/zmisc.cmi
theories/ZArith/znat.cmo: theories/ZArith/znat.cmi
theories/ZArith/znat.cmx: theories/ZArith/znat.cmi
-theories/ZArith/znumtheory.cmo: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
- theories/Init/specif.cmi theories/ZArith/wf_Z.cmi \
- theories/ZArith/zArith_dec.cmi theories/ZArith/zdiv.cmi \
- theories/ZArith/zorder.cmi theories/ZArith/znumtheory.cmi
-theories/ZArith/znumtheory.cmx: theories/ZArith/binInt.cmx \
- theories/NArith/binPos.cmx theories/Init/datatypes.cmx \
- theories/Init/specif.cmx theories/ZArith/wf_Z.cmx \
- theories/ZArith/zArith_dec.cmx theories/ZArith/zdiv.cmx \
- theories/ZArith/zorder.cmx theories/ZArith/znumtheory.cmi
-theories/ZArith/zorder.cmo: theories/ZArith/binInt.cmi \
- theories/Init/datatypes.cmi theories/Init/specif.cmi \
+theories/ZArith/znumtheory.cmo: theories/ZArith/zorder.cmi \
+ theories/ZArith/zdiv.cmi theories/ZArith/zArith_dec.cmi \
+ theories/ZArith/wf_Z.cmi theories/Init/specif.cmi theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi theories/ZArith/znumtheory.cmi
+theories/ZArith/znumtheory.cmx: theories/ZArith/zorder.cmx \
+ theories/ZArith/zdiv.cmx theories/ZArith/zArith_dec.cmx \
+ theories/ZArith/wf_Z.cmx theories/Init/specif.cmx theories/Init/peano.cmx \
+ theories/Init/datatypes.cmx theories/NArith/binPos.cmx \
+ theories/ZArith/binInt.cmx theories/ZArith/znumtheory.cmi
+theories/ZArith/zorder.cmo: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/ZArith/binInt.cmi \
theories/ZArith/zorder.cmi
-theories/ZArith/zorder.cmx: theories/ZArith/binInt.cmx \
- theories/Init/datatypes.cmx theories/Init/specif.cmx \
+theories/ZArith/zorder.cmx: theories/Init/specif.cmx \
+ theories/Init/datatypes.cmx theories/ZArith/binInt.cmx \
theories/ZArith/zorder.cmi
-theories/ZArith/zpower.cmo: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
- theories/ZArith/zmisc.cmi theories/ZArith/zpower.cmi
-theories/ZArith/zpower.cmx: theories/ZArith/binInt.cmx \
- theories/NArith/binPos.cmx theories/Init/datatypes.cmx \
- theories/ZArith/zmisc.cmx theories/ZArith/zpower.cmi
-theories/ZArith/zsqrt.cmo: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Init/specif.cmi \
- theories/ZArith/zArith_dec.cmi theories/ZArith/zsqrt.cmi
-theories/ZArith/zsqrt.cmx: theories/ZArith/binInt.cmx \
- theories/NArith/binPos.cmx theories/Init/specif.cmx \
- theories/ZArith/zArith_dec.cmx theories/ZArith/zsqrt.cmi
+theories/ZArith/zpower.cmo: theories/ZArith/zmisc.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi theories/ZArith/zpower.cmi
+theories/ZArith/zpower.cmx: theories/ZArith/zmisc.cmx \
+ theories/Init/datatypes.cmx theories/NArith/binPos.cmx \
+ theories/ZArith/binInt.cmx theories/ZArith/zpower.cmi
+theories/ZArith/zsqrt.cmo: theories/ZArith/zArith_dec.cmi \
+ theories/Init/specif.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi theories/ZArith/zsqrt.cmi
+theories/ZArith/zsqrt.cmx: theories/ZArith/zArith_dec.cmx \
+ theories/Init/specif.cmx theories/NArith/binPos.cmx \
+ theories/ZArith/binInt.cmx theories/ZArith/zsqrt.cmi
theories/ZArith/zwf.cmo: theories/ZArith/zwf.cmi
theories/ZArith/zwf.cmx: theories/ZArith/zwf.cmi
-theories/Arith/bool_nat.cmi: theories/Arith/compare_dec.cmi \
- theories/Init/datatypes.cmi theories/Arith/peano_dec.cmi \
- theories/Init/specif.cmi theories/Bool/sumbool.cmi
-theories/Arith/compare_dec.cmi: theories/Init/datatypes.cmi \
- theories/Init/specif.cmi
-theories/Arith/compare.cmi: theories/Arith/compare_dec.cmi \
- theories/Init/datatypes.cmi theories/Init/specif.cmi
-theories/Arith/div2.cmi: theories/Init/datatypes.cmi theories/Init/peano.cmi \
- theories/Init/specif.cmi
-theories/Arith/eqNat.cmi: theories/Init/datatypes.cmi \
- theories/Init/specif.cmi
-theories/Arith/euclid.cmi: theories/Arith/compare_dec.cmi \
- theories/Init/datatypes.cmi theories/Init/specif.cmi
-theories/Arith/even.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi
-theories/Arith/factorial.cmi: theories/Init/datatypes.cmi \
- theories/Init/peano.cmi
-theories/Arith/max.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi
-theories/Arith/min.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi
-theories/Arith/mult.cmi: theories/Init/datatypes.cmi theories/Arith/plus.cmi
-theories/Arith/peano_dec.cmi: theories/Init/datatypes.cmi \
- theories/Init/specif.cmi
-theories/Arith/plus.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi
+theories/Arith/bool_nat.cmi: theories/Bool/sumbool.cmi \
+ theories/Init/specif.cmi theories/Arith/peano_dec.cmi \
+ theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi
+theories/Arith/compare_dec.cmi: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi
+theories/Arith/compare.cmi: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi
+theories/Arith/div2.cmi: theories/Init/specif.cmi theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi
+theories/Arith/eqNat.cmi: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi
+theories/Arith/euclid.cmi: theories/Init/specif.cmi theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi
+theories/Arith/even.cmi: theories/Init/specif.cmi theories/Init/datatypes.cmi
+theories/Arith/factorial.cmi: theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi
+theories/Arith/max.cmi: theories/Init/specif.cmi theories/Init/datatypes.cmi
+theories/Arith/min.cmi: theories/Init/specif.cmi theories/Init/datatypes.cmi
+theories/Arith/mult.cmi: theories/Arith/plus.cmi theories/Init/datatypes.cmi
+theories/Arith/peano_dec.cmi: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi
+theories/Arith/plus.cmi: theories/Init/specif.cmi theories/Init/datatypes.cmi
theories/Arith/wf_nat.cmi: theories/Init/datatypes.cmi
-theories/Bool/boolEq.cmi: theories/Init/datatypes.cmi \
- theories/Init/specif.cmi
-theories/Bool/bool.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi
-theories/Bool/bvector.cmi: theories/Bool/bool.cmi theories/Init/datatypes.cmi \
- theories/Init/peano.cmi
+theories/Bool/boolEq.cmi: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi
+theories/Bool/bool.cmi: theories/Init/specif.cmi theories/Init/datatypes.cmi
+theories/Bool/bvector.cmi: theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi theories/Bool/bool.cmi
theories/Bool/decBool.cmi: theories/Init/specif.cmi
-theories/Bool/ifProp.cmi: theories/Init/datatypes.cmi \
- theories/Init/specif.cmi
-theories/Bool/sumbool.cmi: theories/Init/datatypes.cmi \
- theories/Init/specif.cmi
+theories/Bool/ifProp.cmi: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi
+theories/Bool/sumbool.cmi: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi
theories/Bool/zerob.cmi: theories/Init/datatypes.cmi
-theories/Init/logic_Type.cmi: theories/Init/datatypes.cmi
+theories/FSets/decidableTypeEx.cmi: theories/Init/specif.cmi \
+ theories/FSets/orderedTypeEx.cmi theories/FSets/orderedType.cmi \
+ theories/Init/datatypes.cmi
+theories/FSets/decidableType.cmi: theories/Init/specif.cmi
+theories/FSets/fMapAVL.cmi: theories/Init/wf.cmi theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/Lists/list.cmi \
+ theories/FSets/int.cmi theories/Init/datatypes.cmi \
+ theories/NArith/binPos.cmi theories/ZArith/binInt.cmi
+theories/FSets/fMapFacts.cmi: theories/Init/specif.cmi \
+ theories/FSets/fMapInterface.cmi theories/Init/datatypes.cmi
+theories/FSets/fMapInterface.cmi: theories/FSets/orderedType.cmi \
+ theories/Lists/list.cmi theories/Init/datatypes.cmi
+theories/FSets/fMapIntMap.cmi: theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/NArith/ndigits.cmi \
+ theories/IntMap/mapiter.cmi theories/IntMap/mapcanon.cmi \
+ theories/IntMap/map.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binNat.cmi
+theories/FSets/fMapList.cmi: theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi
+theories/FSets/fMapPositive.cmi: theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi
+theories/FSets/fMapWeakFacts.cmi: theories/Init/specif.cmi \
+ theories/Lists/list.cmi theories/FSets/fMapWeakInterface.cmi \
+ theories/Init/datatypes.cmi
+theories/FSets/fMapWeakInterface.cmi: theories/Lists/list.cmi \
+ theories/FSets/decidableType.cmi theories/Init/datatypes.cmi
+theories/FSets/fMapWeakList.cmi: theories/Init/specif.cmi \
+ theories/Lists/list.cmi theories/FSets/decidableType.cmi \
+ theories/Init/datatypes.cmi
+theories/FSets/fSetAVL.cmi: theories/Init/wf.cmi theories/Init/specif.cmi \
+ theories/Init/peano.cmi theories/FSets/orderedType.cmi \
+ theories/Lists/list.cmi theories/FSets/int.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi
+theories/FSets/fSetBridge.cmi: theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/Lists/list.cmi \
+ theories/FSets/fSetInterface.cmi theories/Init/datatypes.cmi
+theories/FSets/fSetEqProperties.cmi: theories/Init/specif.cmi \
+ theories/Setoids/setoid.cmi theories/Init/peano.cmi \
+ theories/FSets/fSetInterface.cmi theories/Init/datatypes.cmi \
+ theories/Bool/bool.cmi
+theories/FSets/fSetFacts.cmi: theories/Init/specif.cmi \
+ theories/Setoids/setoid.cmi theories/FSets/fSetInterface.cmi \
+ theories/Init/datatypes.cmi
+theories/FSets/fSetInterface.cmi: theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi
+theories/FSets/fSetList.cmi: theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi
+theories/FSets/fSetProperties.cmi: theories/Init/specif.cmi \
+ theories/Setoids/setoid.cmi theories/Lists/list.cmi \
+ theories/FSets/fSetInterface.cmi theories/Init/datatypes.cmi
+theories/FSets/fSetToFiniteSet.cmi: theories/Init/specif.cmi \
+ theories/Setoids/setoid.cmi theories/FSets/orderedTypeEx.cmi \
+ theories/FSets/orderedType.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi
+theories/FSets/fSetWeakFacts.cmi: theories/Init/specif.cmi \
+ theories/Setoids/setoid.cmi theories/FSets/fSetWeakInterface.cmi \
+ theories/Init/datatypes.cmi
+theories/FSets/fSetWeakInterface.cmi: theories/Lists/list.cmi \
+ theories/FSets/decidableType.cmi theories/Init/datatypes.cmi
+theories/FSets/fSetWeakList.cmi: theories/Init/specif.cmi \
+ theories/Lists/list.cmi theories/FSets/decidableType.cmi \
+ theories/Init/datatypes.cmi
+theories/FSets/fSetWeakProperties.cmi: theories/Init/specif.cmi \
+ theories/Setoids/setoid.cmi theories/Lists/list.cmi \
+ theories/FSets/fSetWeakInterface.cmi theories/Init/datatypes.cmi
+theories/FSets/int.cmi: theories/ZArith/zmax.cmi \
+ theories/ZArith/zArith_dec.cmi theories/Init/specif.cmi \
+ theories/NArith/binPos.cmi theories/ZArith/binInt.cmi
+theories/FSets/orderedTypeAlt.cmi: theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/Init/datatypes.cmi
+theories/FSets/orderedTypeEx.cmi: theories/Init/specif.cmi \
+ theories/FSets/orderedType.cmi theories/Init/datatypes.cmi \
+ theories/Arith/compare_dec.cmi theories/NArith/binPos.cmi \
+ theories/NArith/binNat.cmi theories/ZArith/binInt.cmi
+theories/FSets/orderedType.cmi: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi
theories/Init/peano.cmi: theories/Init/datatypes.cmi
theories/Init/specif.cmi: theories/Init/datatypes.cmi
-theories/IntMap/adalloc.cmi: theories/IntMap/addec.cmi \
- theories/IntMap/addr.cmi theories/NArith/binPos.cmi \
- theories/Init/datatypes.cmi theories/IntMap/map.cmi \
- theories/Init/specif.cmi theories/Bool/sumbool.cmi
-theories/IntMap/addec.cmi: theories/IntMap/addr.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
- theories/Init/specif.cmi theories/Bool/sumbool.cmi
-theories/IntMap/addr.cmi: theories/NArith/binPos.cmi theories/Bool/bool.cmi \
- theories/Init/datatypes.cmi theories/Init/specif.cmi
-theories/IntMap/adist.cmi: theories/IntMap/addr.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi
-theories/IntMap/fset.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
- theories/Init/datatypes.cmi theories/IntMap/map.cmi \
- theories/Init/specif.cmi
-theories/IntMap/lsort.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
- theories/NArith/binPos.cmi theories/Bool/bool.cmi \
- theories/Init/datatypes.cmi theories/Lists/list.cmi \
- theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \
- theories/Init/specif.cmi theories/Bool/sumbool.cmi
-theories/IntMap/mapcanon.cmi: theories/IntMap/map.cmi \
- theories/Init/specif.cmi
-theories/IntMap/mapcard.cmi: theories/IntMap/addec.cmi \
- theories/IntMap/addr.cmi theories/Init/datatypes.cmi \
- theories/IntMap/map.cmi theories/Init/peano.cmi \
- theories/Arith/peano_dec.cmi theories/Arith/plus.cmi \
- theories/Init/specif.cmi theories/Bool/sumbool.cmi
-theories/IntMap/mapfold.cmi: theories/IntMap/addr.cmi \
- theories/Init/datatypes.cmi theories/IntMap/fset.cmi \
- theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \
- theories/Init/specif.cmi
-theories/IntMap/mapiter.cmi: theories/IntMap/addec.cmi \
- theories/IntMap/addr.cmi theories/Init/datatypes.cmi \
- theories/Lists/list.cmi theories/IntMap/map.cmi theories/Init/specif.cmi \
- theories/Bool/sumbool.cmi
-theories/IntMap/maplists.cmi: theories/IntMap/addec.cmi \
- theories/IntMap/addr.cmi theories/Init/datatypes.cmi \
- theories/IntMap/fset.cmi theories/Lists/list.cmi theories/IntMap/map.cmi \
- theories/IntMap/mapiter.cmi theories/Init/specif.cmi \
- theories/Bool/sumbool.cmi
-theories/IntMap/map.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
- theories/Init/peano.cmi theories/Init/specif.cmi
-theories/IntMap/mapsubset.cmi: theories/Bool/bool.cmi \
- theories/Init/datatypes.cmi theories/IntMap/fset.cmi \
- theories/IntMap/map.cmi theories/IntMap/mapiter.cmi
-theories/Lists/list.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi
-theories/Lists/listSet.cmi: theories/Init/datatypes.cmi \
- theories/Lists/list.cmi theories/Init/specif.cmi
+theories/IntMap/adalloc.cmi: theories/Bool/sumbool.cmi \
+ theories/Init/specif.cmi theories/NArith/ndec.cmi theories/IntMap/map.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/NArith/binNat.cmi
+theories/IntMap/fset.cmi: theories/Init/specif.cmi \
+ theories/NArith/ndigits.cmi theories/NArith/ndec.cmi \
+ theories/IntMap/map.cmi theories/Init/datatypes.cmi \
+ theories/NArith/binNat.cmi
+theories/IntMap/lsort.cmi: theories/Bool/sumbool.cmi theories/Init/specif.cmi \
+ theories/NArith/ndigits.cmi theories/NArith/ndec.cmi \
+ theories/IntMap/mapiter.cmi theories/IntMap/map.cmi \
+ theories/Lists/list.cmi theories/Init/datatypes.cmi \
+ theories/NArith/binNat.cmi
+theories/IntMap/mapcanon.cmi: theories/Init/specif.cmi \
+ theories/IntMap/map.cmi
+theories/IntMap/mapcard.cmi: theories/Bool/sumbool.cmi \
+ theories/Init/specif.cmi theories/Arith/plus.cmi \
+ theories/Arith/peano_dec.cmi theories/Init/peano.cmi \
+ theories/NArith/ndigits.cmi theories/NArith/ndec.cmi \
+ theories/IntMap/map.cmi theories/Init/datatypes.cmi \
+ theories/NArith/binNat.cmi
+theories/IntMap/mapfold.cmi: theories/Init/specif.cmi \
+ theories/IntMap/mapiter.cmi theories/IntMap/map.cmi \
+ theories/IntMap/fset.cmi theories/Init/datatypes.cmi
+theories/IntMap/mapiter.cmi: theories/Bool/sumbool.cmi \
+ theories/Init/specif.cmi theories/NArith/ndigits.cmi \
+ theories/NArith/ndec.cmi theories/IntMap/map.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binNat.cmi
+theories/IntMap/maplists.cmi: theories/Bool/sumbool.cmi \
+ theories/Init/specif.cmi theories/NArith/ndec.cmi \
+ theories/IntMap/mapiter.cmi theories/IntMap/map.cmi \
+ theories/Lists/list.cmi theories/IntMap/fset.cmi \
+ theories/Init/datatypes.cmi
+theories/IntMap/map.cmi: theories/Init/specif.cmi theories/Init/peano.cmi \
+ theories/NArith/ndigits.cmi theories/NArith/ndec.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/NArith/binNat.cmi
+theories/IntMap/mapsubset.cmi: theories/IntMap/mapiter.cmi \
+ theories/IntMap/map.cmi theories/IntMap/fset.cmi \
+ theories/Init/datatypes.cmi theories/Bool/bool.cmi
+theories/Lists/list.cmi: theories/Init/specif.cmi theories/Init/datatypes.cmi
+theories/Lists/listSet.cmi: theories/Init/specif.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi
theories/Lists/monoList.cmi: theories/Init/datatypes.cmi
+theories/Lists/setoidList.cmi: theories/Init/specif.cmi \
+ theories/Lists/list.cmi theories/Init/datatypes.cmi
theories/Lists/streams.cmi: theories/Init/datatypes.cmi
-theories/Lists/theoryList.cmi: theories/Init/datatypes.cmi \
- theories/Lists/list.cmi theories/Init/specif.cmi
-theories/NArith/binNat.cmi: theories/NArith/binPos.cmi \
+theories/Lists/theoryList.cmi: theories/Init/specif.cmi \
+ theories/Lists/list.cmi theories/Init/datatypes.cmi
+theories/Logic/choiceFacts.cmi: theories/Init/specif.cmi \
theories/Init/datatypes.cmi
-theories/NArith/binPos.cmi: theories/Init/datatypes.cmi \
- theories/Init/peano.cmi
-theories/Relations/relation_Operators.cmi: theories/Lists/list.cmi \
- theories/Init/specif.cmi
+theories/Logic/classicalDescription.cmi: theories/Init/specif.cmi \
+ theories/Logic/choiceFacts.cmi
+theories/Logic/classicalEpsilon.cmi: theories/Init/specif.cmi \
+ theories/Logic/choiceFacts.cmi
+theories/Logic/diaconescu.cmi: theories/Init/specif.cmi
+theories/Logic/eqdep_dec.cmi: theories/Init/specif.cmi
+theories/NArith/binNat.cmi: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi
+theories/NArith/binPos.cmi: theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi
+theories/NArith/ndec.cmi: theories/Bool/sumbool.cmi theories/Init/specif.cmi \
+ theories/NArith/nnat.cmi theories/NArith/ndigits.cmi \
+ theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi \
+ theories/NArith/binPos.cmi theories/NArith/binNat.cmi
+theories/NArith/ndigits.cmi: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/Bool/bvector.cmi \
+ theories/Bool/bool.cmi theories/NArith/binPos.cmi \
+ theories/NArith/binNat.cmi
+theories/NArith/ndist.cmi: theories/NArith/ndigits.cmi theories/Arith/min.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/NArith/binNat.cmi
+theories/NArith/nnat.cmi: theories/Init/datatypes.cmi \
+ theories/NArith/binPos.cmi theories/NArith/binNat.cmi
+theories/QArith/qArith_base.cmi: theories/ZArith/zArith_dec.cmi \
+ theories/Init/specif.cmi theories/Setoids/setoid.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi
+theories/QArith/qreals.cmi: theories/QArith/qArith_base.cmi \
+ theories/ZArith/binInt.cmi
+theories/QArith/qreduction.cmi: theories/ZArith/znumtheory.cmi \
+ theories/Setoids/setoid.cmi theories/QArith/qArith_base.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi
+theories/QArith/qring.cmi: theories/Init/specif.cmi \
+ theories/QArith/qArith_base.cmi theories/Init/datatypes.cmi
+theories/Relations/relation_Operators.cmi: theories/Init/specif.cmi \
+ theories/Lists/list.cmi
+theories/Setoids/setoid.cmi: theories/Init/datatypes.cmi
theories/Sets/cpo.cmi: theories/Sets/partial_Order.cmi
-theories/Sets/integers.cmi: theories/Init/datatypes.cmi \
- theories/Sets/partial_Order.cmi
-theories/Sets/multiset.cmi: theories/Init/datatypes.cmi \
- theories/Init/peano.cmi theories/Init/specif.cmi
-theories/Sets/partial_Order.cmi: theories/Sets/ensembles.cmi \
- theories/Sets/relations_1.cmi
-theories/Sets/powerset.cmi: theories/Sets/ensembles.cmi \
- theories/Sets/partial_Order.cmi
-theories/Sets/uniset.cmi: theories/Init/datatypes.cmi \
- theories/Init/specif.cmi
-theories/Sorting/heap.cmi: theories/Init/datatypes.cmi \
- theories/Lists/list.cmi theories/Sets/multiset.cmi \
- theories/Init/peano.cmi theories/Sorting/sorting.cmi \
- theories/Init/specif.cmi
-theories/Sorting/permutation.cmi: theories/Init/datatypes.cmi \
- theories/Lists/list.cmi theories/Sets/multiset.cmi \
- theories/Init/peano.cmi theories/Init/specif.cmi
-theories/Sorting/sorting.cmi: theories/Lists/list.cmi \
- theories/Init/specif.cmi
-theories/Wellfounded/well_Ordering.cmi: theories/Init/specif.cmi
-theories/ZArith/binInt.cmi: theories/NArith/binNat.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi
-theories/ZArith/wf_Z.cmi: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
- theories/Init/peano.cmi theories/Init/specif.cmi
-theories/ZArith/zabs.cmi: theories/ZArith/binInt.cmi theories/Init/specif.cmi \
- theories/Bool/sumbool.cmi
-theories/ZArith/zArith_dec.cmi: theories/ZArith/binInt.cmi \
- theories/Init/datatypes.cmi theories/Init/specif.cmi \
- theories/Bool/sumbool.cmi
-theories/ZArith/zbinary.cmi: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Bool/bvector.cmi \
- theories/Init/datatypes.cmi theories/ZArith/zeven.cmi
-theories/ZArith/zbool.cmi: theories/ZArith/binInt.cmi \
- theories/Init/datatypes.cmi theories/Init/specif.cmi \
- theories/Bool/sumbool.cmi theories/ZArith/zArith_dec.cmi \
- theories/ZArith/zeven.cmi
-theories/ZArith/zcomplements.cmi: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
- theories/Lists/list.cmi theories/Init/specif.cmi theories/ZArith/wf_Z.cmi \
- theories/ZArith/zabs.cmi
-theories/ZArith/zdiv.cmi: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
- theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \
- theories/ZArith/zbool.cmi
-theories/ZArith/zeven.cmi: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
- theories/Init/specif.cmi
-theories/ZArith/zlogarithm.cmi: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi
-theories/ZArith/zmin.cmi: theories/ZArith/binInt.cmi \
+theories/Sets/integers.cmi: theories/Sets/partial_Order.cmi \
theories/Init/datatypes.cmi
-theories/ZArith/zmisc.cmi: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi
-theories/ZArith/znumtheory.cmi: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
- theories/Init/specif.cmi theories/ZArith/wf_Z.cmi \
- theories/ZArith/zArith_dec.cmi theories/ZArith/zdiv.cmi \
- theories/ZArith/zorder.cmi
-theories/ZArith/zorder.cmi: theories/ZArith/binInt.cmi \
- theories/Init/datatypes.cmi theories/Init/specif.cmi
-theories/ZArith/zpower.cmi: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Init/datatypes.cmi \
- theories/ZArith/zmisc.cmi
-theories/ZArith/zsqrt.cmi: theories/ZArith/binInt.cmi \
- theories/NArith/binPos.cmi theories/Init/specif.cmi \
- theories/ZArith/zArith_dec.cmi
+theories/Sets/multiset.cmi: theories/Init/specif.cmi theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi
+theories/Sets/partial_Order.cmi: theories/Sets/relations_1.cmi \
+ theories/Sets/ensembles.cmi
+theories/Sets/powerset.cmi: theories/Sets/partial_Order.cmi \
+ theories/Sets/ensembles.cmi
+theories/Sets/uniset.cmi: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi
+theories/Sorting/heap.cmi: theories/Init/specif.cmi \
+ theories/Sorting/sorting.cmi theories/Init/peano.cmi \
+ theories/Sets/multiset.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi
+theories/Sorting/permutation.cmi: theories/Init/specif.cmi \
+ theories/Init/peano.cmi theories/Sets/multiset.cmi \
+ theories/Lists/list.cmi theories/Init/datatypes.cmi
+theories/Sorting/sorting.cmi: theories/Init/specif.cmi \
+ theories/Lists/list.cmi
+theories/Strings/ascii.cmi: theories/Init/specif.cmi theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi theories/Bool/bool.cmi \
+ theories/NArith/binPos.cmi
+theories/Strings/string.cmi: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/Strings/ascii.cmi
+theories/Wellfounded/well_Ordering.cmi: theories/Init/specif.cmi
+theories/ZArith/binInt.cmi: theories/Init/datatypes.cmi \
+ theories/NArith/binPos.cmi theories/NArith/binNat.cmi
+theories/ZArith/wf_Z.cmi: theories/Init/specif.cmi theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi
+theories/ZArith/zabs.cmi: theories/Init/specif.cmi theories/ZArith/binInt.cmi
+theories/ZArith/zArith_dec.cmi: theories/Bool/sumbool.cmi \
+ theories/Init/specif.cmi theories/Init/datatypes.cmi \
+ theories/ZArith/binInt.cmi
+theories/ZArith/zbinary.cmi: theories/ZArith/zeven.cmi \
+ theories/Init/datatypes.cmi theories/Bool/bvector.cmi \
+ theories/NArith/binPos.cmi theories/ZArith/binInt.cmi
+theories/ZArith/zbool.cmi: theories/ZArith/zeven.cmi \
+ theories/ZArith/zArith_dec.cmi theories/Bool/sumbool.cmi \
+ theories/Init/specif.cmi theories/Init/datatypes.cmi \
+ theories/ZArith/binInt.cmi
+theories/ZArith/zcomplements.cmi: theories/ZArith/zabs.cmi \
+ theories/ZArith/wf_Z.cmi theories/Init/specif.cmi theories/Lists/list.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi
+theories/ZArith/zdiv.cmi: theories/ZArith/zbool.cmi \
+ theories/ZArith/zArith_dec.cmi theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi
+theories/ZArith/zeven.cmi: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi
+theories/ZArith/zlogarithm.cmi: theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi
+theories/ZArith/zmax.cmi: theories/Init/datatypes.cmi \
+ theories/ZArith/binInt.cmi
+theories/ZArith/zmin.cmi: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/ZArith/binInt.cmi
+theories/ZArith/zmisc.cmi: theories/Init/datatypes.cmi \
+ theories/NArith/binPos.cmi theories/ZArith/binInt.cmi
+theories/ZArith/znumtheory.cmi: theories/ZArith/zorder.cmi \
+ theories/ZArith/zdiv.cmi theories/ZArith/zArith_dec.cmi \
+ theories/ZArith/wf_Z.cmi theories/Init/specif.cmi theories/Init/peano.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi
+theories/ZArith/zorder.cmi: theories/Init/specif.cmi \
+ theories/Init/datatypes.cmi theories/ZArith/binInt.cmi
+theories/ZArith/zpower.cmi: theories/ZArith/zmisc.cmi \
+ theories/Init/datatypes.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi
+theories/ZArith/zsqrt.cmi: theories/ZArith/zArith_dec.cmi \
+ theories/Init/specif.cmi theories/NArith/binPos.cmi \
+ theories/ZArith/binInt.cmi
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index c9bb5623..65a54090 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -10,7 +10,7 @@ AXIOMSVO:= \
theories/Reals/% \
theories/Num/%
-DIRS:= $(shell (cd $(TOPDIR);find theories -type d ! -name CVS))
+DIRS:= $(shell (cd $(TOPDIR);find theories -type d ! -path \*.svn\*))
INCL:= $(patsubst %,-I %,$(DIRS))
@@ -34,7 +34,7 @@ all: v2ml ml $(MLI) $(CMO)
ml: $(ML)
-depend: $(ML)
+depend: #$(ML)
rm -f .depend; ocamldep $(INCL) theories/*/*.ml theories/*/*.mli > .depend
tree:
diff --git a/contrib/extraction/test/custom/Adalloc b/contrib/extraction/test/custom/Adalloc
index 0fb556aa..e7204838 100644
--- a/contrib/extraction/test/custom/Adalloc
+++ b/contrib/extraction/test/custom/Adalloc
@@ -1,2 +1,2 @@
-Require Import Addr.
-Extraction NoInline ad_double ad_double_plus_un.
+Require Import BinNat.
+Extraction NoInline Ndouble Ndouble_plus_one.
diff --git a/contrib/extraction/test/custom/Lsort b/contrib/extraction/test/custom/Lsort
index 6a185683..22ab18e3 100644
--- a/contrib/extraction/test/custom/Lsort
+++ b/contrib/extraction/test/custom/Lsort
@@ -1,2 +1,2 @@
-Require Import Addr.
-Extraction NoInline ad_double ad_double_plus_un.
+Require Import BinNat.
+Extraction NoInline Ndouble Ndouble_plus_one.
diff --git a/contrib/extraction/test/custom/Map b/contrib/extraction/test/custom/Map
index 3e464e39..f024dbd7 100644
--- a/contrib/extraction/test/custom/Map
+++ b/contrib/extraction/test/custom/Map
@@ -1,3 +1,3 @@
-Require Import Addr.
-Extraction NoInline ad_double ad_double_plus_un.
+Require Import BinNat.
+Extraction NoInline Ndouble Ndouble_plus_one.
diff --git a/contrib/extraction/test/custom/Mapcard b/contrib/extraction/test/custom/Mapcard
index ca555aa3..5932cf7b 100644
--- a/contrib/extraction/test/custom/Mapcard
+++ b/contrib/extraction/test/custom/Mapcard
@@ -1,4 +1,4 @@
Require Import Plus.
Extraction NoInline plus_is_one.
-Require Import Addr.
-Extraction NoInline ad_double ad_double_plus_un.
+Require Import BinNat.
+Extraction NoInline Ndouble Ndouble_plus_one.
diff --git a/contrib/extraction/test/custom/Mapiter b/contrib/extraction/test/custom/Mapiter
index 6a185683..22ab18e3 100644
--- a/contrib/extraction/test/custom/Mapiter
+++ b/contrib/extraction/test/custom/Mapiter
@@ -1,2 +1,2 @@
-Require Import Addr.
-Extraction NoInline ad_double ad_double_plus_un.
+Require Import BinNat.
+Extraction NoInline Ndouble Ndouble_plus_one.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-03 15:44:07 +0000