diff options
Diffstat (limited to 'contrib/extraction')
| -rw-r--r-- | contrib/extraction/common.ml | 47 | ||||
| -rw-r--r-- | contrib/extraction/extraction.ml | 183 | ||||
| -rw-r--r-- | contrib/extraction/haskell.ml | 22 | ||||
| -rw-r--r-- | contrib/extraction/miniml.mli | 17 | ||||
| -rw-r--r-- | contrib/extraction/mlutil.ml | 87 | ||||
| -rw-r--r-- | contrib/extraction/mlutil.mli | 18 | ||||
| -rw-r--r-- | contrib/extraction/modutil.ml | 48 | ||||
| -rw-r--r-- | contrib/extraction/modutil.mli | 4 | ||||
| -rw-r--r-- | contrib/extraction/ocaml.ml | 13 | ||||
| -rw-r--r-- | contrib/extraction/test/.depend | 1417 | ||||
| -rw-r--r-- | contrib/extraction/test/Makefile | 4 | ||||
| -rw-r--r-- | contrib/extraction/test/custom/Adalloc | 4 | ||||
| -rw-r--r-- | contrib/extraction/test/custom/Lsort | 4 | ||||
| -rw-r--r-- | contrib/extraction/test/custom/Map | 4 | ||||
| -rw-r--r-- | contrib/extraction/test/custom/Mapcard | 4 | ||||
| -rw-r--r-- | contrib/extraction/test/custom/Mapiter | 4 |
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. |