diff options
45 files changed, 288 insertions, 235 deletions
diff --git a/dev/include b/dev/include index 15725ae8b..f785573ce 100644 --- a/dev/include +++ b/dev/include @@ -45,7 +45,7 @@ #install_printer (* Goal.goal *) ppgoalgoal;; #install_printer (* metaset.t *) ppmetas;; #install_printer (* evar_map *) ppevm;; -#install_printer (* ExistentialSet.t *) ppexistentialset;; +#install_printer (* Evar.Set.t *) ppexistentialset;; #install_printer (* clenv *) ppclenv;; #install_printer (* env *) ppenv;; diff --git a/dev/printers.mllib b/dev/printers.mllib index 8e99b5247..1eb3aa4bb 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -45,6 +45,7 @@ Names Univ Esubst Sorts +Evar Constr Context Vars diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 89e2d7ddd..6bb352c5e 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -106,11 +106,12 @@ let pp_cpred s = pp (pr_cpred s) let pp_transparent_state s = pp (pr_transparent_state s) (* proof printers *) +let pr_evar ev = Pp.int (Evar.repr ev) let ppmetas metas = pp(pr_metaset metas) let ppevm evd = pp(pr_evar_map (Some 2) evd) let ppevmall evd = pp(pr_evar_map None evd) let pr_existentialset evars = - prlist_with_sep spc pr_meta (ExistentialSet.elements evars) + prlist_with_sep spc pr_evar (Evar.Set.elements evars) let ppexistentialset evars = pp (pr_existentialset evars) let ppclenv clenv = pp(pr_clenv clenv) @@ -172,7 +173,7 @@ let constr_display csr = "LetIn("^(name_display na)^","^(term_display b)^"," ^(term_display t)^","^(term_display c)^")" | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n" - | Evar (e,l) -> "Evar("^(string_of_int e)^","^(array_display l)^")" + | Evar (e,l) -> "Evar("^(string_of_existential e)^","^(array_display l)^")" | Const c -> "Const("^(string_of_con c)^")" | Ind (sp,i) -> "MutInd("^(string_of_mind sp)^","^(string_of_int i)^")" @@ -250,7 +251,7 @@ let print_pure_constr csr = box_display c; Array.iter (fun x -> print_space (); box_display x) l; print_string ")" - | Evar (e,l) -> print_string "Evar#"; print_int e; print_string "{"; + | Evar (e,l) -> print_string "Evar#"; print_int (Evar.repr e); print_string "{"; Array.iter (fun x -> print_space (); box_display x) l; print_string"}" | Const c -> print_string "Cons("; diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 50c1cfa6a..b1c1c3c8e 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -26,6 +26,7 @@ Segmenttree Unicodetable Unicode +Evar Names Libnames Genarg diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 28faa2ce6..5edfc0614 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -147,7 +147,7 @@ let rec constr_expr_eq e1 e2 = | CPatVar(_,(b1, i1)), CPatVar(_,(b2, i2)) -> (b1 : bool) == b2 && Id.equal i1 i2 | CEvar (_, ev1, c1), CEvar (_, ev2, c2) -> - Int.equal ev1 ev2 && + Evar.equal ev1 ev2 && Option.equal (List.equal constr_expr_eq) c1 c2 | CSort(_,s1), CSort(_,s2) -> Glob_ops.glob_sort_eq s1 s2 diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 91fdf3829..6ee44215c 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -40,9 +40,9 @@ type 'id move_location = type sort_info = string option type glob_sort = GProp | GSet | GType of sort_info -(** A synonym of [int], also defined in Term *) +(** A synonym of [Evar.t], also defined in Term *) -type existential_key = int +type existential_key = Evar.t (** Case style, shared with Term *) diff --git a/kernel/constr.ml b/kernel/constr.ml index eba490dbd..8b7505aeb 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -31,7 +31,7 @@ open Univ open Esubst -type existential_key = int +type existential_key = Evar.t type metavariable = int (* This defines the strategy to use for verifiying a Cast *) @@ -341,7 +341,7 @@ let compare_head f t1 t2 = | App (c1,l1), App (c2,l2) -> Int.equal (Array.length l1) (Array.length l2) && f c1 c2 && Array.equal f l1 l2 - | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal f l1 l2 | Const c1, Const c2 -> eq_constant c1 c2 | Ind c1, Ind c2 -> eq_ind c1 c2 | Construct c1, Construct c2 -> eq_constructor c1 c2 @@ -391,7 +391,7 @@ let constr_ord_int f t1 t2 = | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2)) | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2 | Evar (e1,l1), Evar (e2,l2) -> - ((-) =? (Array.compare f)) e1 e2 l1 l2 + (Evar.compare =? (Array.compare f)) e1 e2 l1 l2 | Const c1, Const c2 -> con_ord c1 c2 | Ind ind1, Ind ind2 -> ind_ord ind1 ind2 | Construct ct1, Construct ct2 -> constructor_ord ct1 ct2 @@ -469,7 +469,7 @@ let hasheq t1 t2 = | LetIn (n1,b1,t1,c1), LetIn (n2,b2,t2,c2) -> n1 == n2 & b1 == b2 & t1 == t2 & c1 == c2 | App (c1,l1), App (c2,l2) -> c1 == c2 & array_eqeq l1 l2 - | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 & array_eqeq l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 & array_eqeq l1 l2 | Const c1, Const c2 -> c1 == c2 | Ind (sp1,i1), Ind (sp2,i2) -> sp1 == sp2 && Int.equal i1 i2 | Construct ((sp1,i1),j1), Construct ((sp2,i2),j2) -> diff --git a/kernel/constr.mli b/kernel/constr.mli index 59430125f..261b6bfb4 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -9,7 +9,7 @@ open Names (** {6 Existential variables } *) -type existential_key = int +type existential_key = Evar.t (** {6 Existential variables } *) type metavariable = int diff --git a/kernel/evar.ml b/kernel/evar.ml new file mode 100644 index 000000000..d7e32626f --- /dev/null +++ b/kernel/evar.ml @@ -0,0 +1,24 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type t = int + +let repr x = x +let unsafe_of_int x = x +let compare = Int.compare +let equal = Int.equal + +module Self = +struct + type _t = t + type t = _t + let compare = compare +end + +module Set = Set.Make(Self) +module Map = CMap.Make(Self) diff --git a/kernel/evar.mli b/kernel/evar.mli new file mode 100644 index 000000000..8e8b88d94 --- /dev/null +++ b/kernel/evar.mli @@ -0,0 +1,31 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** This module defines existential variables, which are isomorphic to [int]. + Nonetheless, casting from an [int] to a variable is deemed unsafe, so that + to keep track of such casts, one has to use the provided {!unsafe_of_int} + function. *) + +type t +(** Type of existential variables. *) + +val repr : t -> int +(** Recover the underlying integer. *) + +val unsafe_of_int : int -> t +(** This is not for dummies. Do not use this function if you don't know what you + are doing. *) + +val equal : t -> t -> bool +(** Equality over existential variables. *) + +val compare : t -> t -> int +(** Comparison over existential variables. *) + +module Set : Set.S with type elt = t +module Map : CMap.ExtS with type key = t and module Set := Set diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 36b3d8323..cbc147e9e 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -2,6 +2,7 @@ Names Univ Esubst Sorts +Evar Constr Context Vars diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 1f5a6a6a0..48c63ac96 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -277,7 +277,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = else raise NotConvertible | _ -> raise NotConvertible) | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) -> - if Int.equal ev1 ev2 then + if Evar.equal ev1 ev2 then let u1 = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in convert_vect l2r infos el1 el2 (Array.map (mk_clos env1) args1) diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 982b71ba0..6e6612e9a 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -133,7 +133,7 @@ let get_xml_name al = ident_of_cdata (get_xml_attr "name" al) let get_xml_noFun al = nmtoken (get_xml_attr "noFun" al) -let get_xml_no al = nmtoken (get_xml_attr "no" al) +let get_xml_no al = Evar.unsafe_of_int (nmtoken (get_xml_attr "no" al)) (* A leak in the xml dtd: arities of constructor need to know global env *) diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 355a18005..f16c298af 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -35,10 +35,13 @@ open Misctypes (****************************************************************************) (* controlled reduction *) -let mark_arg i c = mkEvar(i,[|c|]) +(** ppedrot: something dubious here, we're obviously using evars the wrong + way. FIXME! *) + +let mark_arg i c = mkEvar(Evar.unsafe_of_int i,[|c|]) let unmark_arg f c = match destEvar c with - | (i,[|c|]) -> f i c + | (i,[|c|]) -> f (Evar.repr i) c | _ -> assert false type protect_flag = Eval|Prot|Rec diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4 index 9d3a10dba..73f113d6a 100644 --- a/plugins/xml/acic2Xml.ml4 +++ b/plugins/xml/acic2Xml.ml4 @@ -26,7 +26,7 @@ let rec find_last_id = | _::tl -> find_last_id tl ;; -let export_existential = string_of_int +let export_existential ev = string_of_int (Evar.repr ev) let print_term ids_to_inner_sorts = let rec aux = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 9483f0220..1588856f7 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -391,7 +391,7 @@ let rec detype (isgoal:bool) avoid env t = in GVar (dl, Id.of_string s)) | Meta n -> (* Meta in constr are not user-parsable and are mapped to Evar *) - GEvar (dl, n, None) + GEvar (dl, Evar.unsafe_of_int n, None) | Var id -> (try let _ = Global.lookup_named id in GRef (dl, VarRef id) with Not_found -> GVar (dl, id)) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 7724261ec..6d4f214cc 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -338,7 +338,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (i,NotSameArgSize) and f2 i = - if Int.equal sp1 sp2 then + if Evar.equal sp1 sp2 then match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with |None, Success i' -> Success (solve_refl (fun env i pbty a1 a2 -> @@ -805,7 +805,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = (match choose_less_dependent_instance evk2 evd term1 args2 with | Some evd -> Success evd | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))) - | Evar (evk1,args1), Evar (evk2,args2) when Int.equal evk1 evk2 -> + | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> let f env evd pbty x y = is_trans_fconv pbty ts env evd x y in Success (solve_refl ~can_drop:true f env evd evk1 args1 args2) | Evar ev1, Evar ev2 -> diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 52088af38..a1bf6eabb 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -114,7 +114,7 @@ let noccur_evar env evd evk c = (match safe_evar_value evd ev' with | Some c -> occur_rec k c | None -> - if Int.equal evk evk' then raise Occur + if Evar.equal evk evk' then raise Occur else Array.iter (occur_rec k) args') | Rel i when i > k -> (match pi2 (Environ.lookup_rel (i-k) env) with @@ -956,7 +956,7 @@ let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t = Array.for_all (is_constrainable_in k g) params | Ind _ -> Array.for_all (is_constrainable_in k g) args | Prod (_,t1,t2) -> is_constrainable_in k g t1 && is_constrainable_in k g t2 - | Evar (ev',_) -> not (Int.equal ev' ev) (*If ev' needed, one may also try to restrict it*) + | Evar (ev',_) -> not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*) | Var id -> Id.Set.mem id fv_ids | Rel n -> n <= k || Int.Set.mem n fv_rels | Sort _ -> true @@ -1068,7 +1068,7 @@ let solve_refl ?(can_drop=false) conv_algo env evd evk argsv1 argsv2 = let candidates = filter_candidates evd evk untypedfilter None in let filter = closure_of_filter evd evk untypedfilter in let evd,ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in - if Int.equal (fst ev1) evk && can_drop then (* No refinement *) evd else + if Evar.equal (fst ev1) evk && can_drop then (* No refinement *) evd else (* either progress, or not allowed to drop, e.g. to preserve possibly *) (* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *) (* if e can depend on x until ?y is not resolved, or, conversely, we *) @@ -1198,7 +1198,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = try project_variable t with NotInvertibleUsingOurAlgorithm _ -> imitate envk b) | Evar (evk',args' as ev') -> - if Int.equal evk evk' then raise (OccurCheckIn (evd,rhs)); + if Evar.equal evk evk' then raise (OccurCheckIn (evd,rhs)); (* Evar/Evar problem (but left evar is virtual) *) let aliases = lift_aliases k aliases in (try @@ -1278,7 +1278,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs = match kind_of_term rhs with | Evar (evk2,argsv2 as ev2) -> - if Int.equal evk evk2 then + if Evar.equal evk evk2 then solve_refl ~can_drop:choose (test_success conv_algo) env evd evk argsv argsv2 else @@ -1322,7 +1322,7 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs = (* last chance: rhs actually reduces to ev *) let c = whd_betadeltaiota env evd rhs in match kind_of_term c with - | Evar (evk',argsv2) when Int.equal evk evk' -> + | Evar (evk',argsv2) when Evar.equal evk evk' -> solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c') env evd evk argsv argsv2 | _ -> @@ -1355,8 +1355,8 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs = *) let status_changed lev (pbty,_,t1,t2) = - (try ExistentialSet.mem (head_evar t1) lev with NoHeadEvar -> false) or - (try ExistentialSet.mem (head_evar t2) lev with NoHeadEvar -> false) + (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) or + (try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false) let reconsider_conv_pbs conv_algo evd = let (evd,pbs) = extract_changed_conv_pbs evd status_changed in diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index b1dec0fd0..f66e5f708 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -233,7 +233,7 @@ let evars_to_metas sigma (emap, c) = let non_instantiated sigma = let listev = Evd.undefined_map sigma in - ExistentialMap.map (fun evi -> nf_evar_info sigma evi) listev + Evar.Map.map (fun evi -> nf_evar_info sigma evi) listev (************************) (* Manipulating filters *) @@ -257,7 +257,7 @@ let make_pure_subst evi args = (* Generator of existential names *) let new_untyped_evar = let evar_ctr = Summary.ref 0 ~name:"evar counter" in - fun () -> incr evar_ctr; existential_of_int !evar_ctr + fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr (*------------------------------------* * functional operations on evar sets * @@ -486,14 +486,14 @@ let clear_hyps_in_evi evdref hyps concl ids = let evars_of_term c = let rec evrec acc c = match kind_of_term c with - | Evar (n, l) -> Int.Set.add n (Array.fold_left evrec acc l) + | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) | _ -> fold_constr evrec acc c in - evrec Int.Set.empty c + evrec Evar.Set.empty c (* spiwack: a few functions to gather evars on which goals depend. *) let queue_set q is_dependent set = - Int.Set.iter (fun a -> Queue.push (is_dependent,a) q) set + Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set let queue_term q is_dependent c = queue_set q is_dependent (evars_of_term c) @@ -510,7 +510,7 @@ let process_dependent_evar q acc evm is_dependent e = end (Environ.named_context_of_val evi.evar_hyps); match evi.evar_body with | Evar_empty -> - if is_dependent then Int.Map.add e None acc else acc + if is_dependent then Evar.Map.add e None acc else acc | Evar_defined b -> let subevars = evars_of_term b in (* evars appearing in the definition of an evar [e] are marked @@ -518,14 +518,14 @@ let process_dependent_evar q acc evm is_dependent e = non-dependent goal, then, unless they are reach from another path, these evars are just other non-dependent goals. *) queue_set q is_dependent subevars; - if is_dependent then Int.Map.add e (Some subevars) acc else acc + if is_dependent then Evar.Map.add e (Some subevars) acc else acc let gather_dependent_evars q evm = - let acc = ref Int.Map.empty in + let acc = ref Evar.Map.empty in while not (Queue.is_empty q) do let (is_dependent,e) = Queue.pop q in (* checks if [e] has already been added to [!acc] *) - begin if not (Int.Map.mem e !acc) then + begin if not (Evar.Map.mem e !acc) then acc := process_dependent_evar q !acc evm is_dependent e end done; @@ -541,15 +541,15 @@ let gather_dependent_evars evm l = let evars_of_named_context nc = List.fold_right (fun (_, b, t) s -> Option.fold_left (fun s t -> - Int.Set.union s (evars_of_term t)) - (Int.Set.union s (evars_of_term t)) b) - nc Int.Set.empty + Evar.Set.union s (evars_of_term t)) + (Evar.Set.union s (evars_of_term t)) b) + nc Evar.Set.empty let evars_of_evar_info evi = - Int.Set.union (evars_of_term evi.evar_concl) - (Int.Set.union + Evar.Set.union (evars_of_term evi.evar_concl) + (Evar.Set.union (match evi.evar_body with - | Evar_empty -> Int.Set.empty + | Evar_empty -> Evar.Set.empty | Evar_defined b -> evars_of_term b) (evars_of_named_context (named_context_of_val evi.evar_hyps))) @@ -564,25 +564,25 @@ let undefined_evars_of_term evd t = | Evar (n, l) -> let acc = Array.fold_left evrec acc l in (try match (Evd.find evd n).evar_body with - | Evar_empty -> Int.Set.add n acc + | Evar_empty -> Evar.Set.add n acc | Evar_defined c -> evrec acc c with Not_found -> anomaly ~label:"undefined_evars_of_term" (Pp.str "evar not found")) | _ -> fold_constr evrec acc c in - evrec Int.Set.empty t + evrec Evar.Set.empty t let undefined_evars_of_named_context evd nc = List.fold_right (fun (_, b, t) s -> Option.fold_left (fun s t -> - Int.Set.union s (undefined_evars_of_term evd t)) - (Int.Set.union s (undefined_evars_of_term evd t)) b) - nc Int.Set.empty + Evar.Set.union s (undefined_evars_of_term evd t)) + (Evar.Set.union s (undefined_evars_of_term evd t)) b) + nc Evar.Set.empty let undefined_evars_of_evar_info evd evi = - Int.Set.union (undefined_evars_of_term evd evi.evar_concl) - (Int.Set.union + Evar.Set.union (undefined_evars_of_term evd evi.evar_concl) + (Evar.Set.union (match evi.evar_body with - | Evar_empty -> Int.Set.empty + | Evar_empty -> Evar.Set.empty | Evar_defined b -> undefined_evars_of_term evd b) (undefined_evars_of_named_context evd (named_context_of_val evi.evar_hyps))) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 0d482e9b0..d146bca47 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -66,7 +66,7 @@ val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list returns the evar_map extended with dependent evars *) val evars_to_metas : evar_map -> open_constr -> (evar_map * constr) -val non_instantiated : evar_map -> evar_info ExistentialMap.t +val non_instantiated : evar_map -> evar_info Evar.Map.t (** {6 Unification utils} *) @@ -98,10 +98,10 @@ val evar_absorb_arguments : env -> evar_map -> existential -> constr list -> contained in the object, including defined evars *) -val evars_of_term : constr -> Int.Set.t +val evars_of_term : constr -> Evar.Set.t -val evars_of_named_context : named_context -> Int.Set.t -val evars_of_evar_info : evar_info -> Int.Set.t +val evars_of_named_context : named_context -> Evar.Set.t +val evars_of_evar_info : evar_info -> Evar.Set.t (** [gather_dependent_evars evm seeds] classifies the evars in [evm] as dependent_evars and goals (these may overlap). A goal is an @@ -112,16 +112,16 @@ val evars_of_evar_info : evar_info -> Int.Set.t associating to each dependent evar [None] if it has no (partial) definition or [Some s] if [s] is the list of evars appearing in its (partial) definition. *) -val gather_dependent_evars : evar_map -> evar list -> (Int.Set.t option) Int.Map.t +val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.Map.t (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. This is roughly a combination of the previous functions and [nf_evar]. *) -val undefined_evars_of_term : evar_map -> constr -> Int.Set.t -val undefined_evars_of_named_context : evar_map -> named_context -> Int.Set.t -val undefined_evars_of_evar_info : evar_map -> evar_info -> Int.Set.t +val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t +val undefined_evars_of_named_context : evar_map -> named_context -> Evar.Set.t +val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t (** {6 Value/Type constraints} *) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index cebce3abe..1aa899771 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -27,8 +27,7 @@ module Store = Store.Make(Dummy) type evar = Term.existential_key -let string_of_existential evk = "?" ^ string_of_int evk -let existential_of_int evk = evk +let string_of_existential evk = "?" ^ string_of_int (Evar.repr evk) type evar_body = | Evar_empty @@ -81,15 +80,12 @@ let eq_evar_info ei1 ei2 = (** ppedrot: [eq_constr] may be a bit too permissive here *) (* spiwack: Revised hierarchy : - - ExistentialMap ( Maps of existential_keys ) - - EvarInfoMap ( .t = evar_info ExistentialMap.t * evar_info ExistentialMap ) + - Evar.Map ( Maps of existential_keys ) + - EvarInfoMap ( .t = evar_info Evar.Map.t * evar_info Evar.Map ) - EvarMap ( .t = EvarInfoMap.t * sort_constraints ) - evar_map (exported) *) -module ExistentialMap = Int.Map -module ExistentialSet = Int.Set - (* This exception is raised by *.existential_value *) exception NotInstantiatedEvar @@ -195,70 +191,70 @@ let metamap_to_list m = type conv_pb = Reduction.conv_pb type evar_constraint = conv_pb * Environ.env * constr * constr +module EvMap = Evar.Map + type evar_map = { - defn_evars : evar_info ExistentialMap.t; - undf_evars : evar_info ExistentialMap.t; + defn_evars : evar_info EvMap.t; + undf_evars : evar_info EvMap.t; universes : Univ.UniverseLSet.t; univ_cstrs : Univ.universes; conv_pbs : evar_constraint list; - last_mods : ExistentialSet.t; + last_mods : Evar.Set.t; metas : clbinding Metamap.t } -module ExMap = ExistentialMap - (*** Lifting primitive from EvarMap. ***) (* HH: The progress tactical now uses this function. *) let progress_evar_map d1 d2 = let is_new k v = assert (v.evar_body == Evar_empty); - ExMap.mem k d2.defn_evars + EvMap.mem k d2.defn_evars in - not (d1 == d2) && ExMap.exists is_new d1.undf_evars + not (d1 == d2) && EvMap.exists is_new d1.undf_evars let add d e i = match i.evar_body with | Evar_empty -> - { d with undf_evars = ExMap.add e i d.undf_evars; } + { d with undf_evars = EvMap.add e i d.undf_evars; } | Evar_defined _ -> - { d with defn_evars = ExMap.add e i d.defn_evars; } + { d with defn_evars = EvMap.add e i d.defn_evars; } let remove d e = - let undf_evars = ExMap.remove e d.undf_evars in - let defn_evars = ExMap.remove e d.defn_evars in + let undf_evars = EvMap.remove e d.undf_evars in + let defn_evars = EvMap.remove e d.defn_evars in { d with undf_evars; defn_evars; } let find d e = - try ExMap.find e d.undf_evars - with Not_found -> ExMap.find e d.defn_evars + try EvMap.find e d.undf_evars + with Not_found -> EvMap.find e d.defn_evars -let find_undefined d e = ExMap.find e d.undf_evars +let find_undefined d e = EvMap.find e d.undf_evars -let mem d e = ExMap.mem e d.undf_evars || ExMap.mem e d.defn_evars +let mem d e = EvMap.mem e d.undf_evars || EvMap.mem e d.defn_evars (* spiwack: this function loses information from the original evar_map it might be an idea not to export it. *) let to_list d = (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *) let l = ref [] in - ExistentialMap.iter (fun evk x -> l := (evk,x)::!l) d.defn_evars; - ExistentialMap.iter (fun evk x -> l := (evk,x)::!l) d.undf_evars; + EvMap.iter (fun evk x -> l := (evk,x)::!l) d.defn_evars; + EvMap.iter (fun evk x -> l := (evk,x)::!l) d.undf_evars; !l let undefined_map d = d.undf_evars let defined_map d = d.defn_evars -let undefined_evars d = { d with defn_evars = ExMap.empty } +let undefined_evars d = { d with defn_evars = EvMap.empty } -let defined_evars d = { d with undf_evars = ExMap.empty } +let defined_evars d = { d with undf_evars = EvMap.empty } (* spiwack: not clear what folding over an evar_map, for now we shall simply fold over the inner evar_map. *) let fold f d a = - ExMap.fold f d.defn_evars (ExMap.fold f d.undf_evars a) + EvMap.fold f d.defn_evars (EvMap.fold f d.undf_evars a) -let fold_undefined f d a = ExMap.fold f d.undf_evars a +let fold_undefined f d a = EvMap.fold f d.undf_evars a let raw_map f d = let f evk info = @@ -271,8 +267,8 @@ let raw_map f d = in ans in - let defn_evars = ExMap.mapi f d.defn_evars in - let undf_evars = ExMap.mapi f d.undf_evars in + let defn_evars = EvMap.mapi f d.defn_evars in + let undf_evars = EvMap.mapi f d.undf_evars in { d with defn_evars; undf_evars; } let raw_map_undefined f d = @@ -285,13 +281,13 @@ let raw_map_undefined f d = in ans in - { d with undf_evars = ExMap.mapi f d.undf_evars; } + { d with undf_evars = EvMap.mapi f d.undf_evars; } let is_evar = mem -let is_defined d e = ExMap.mem e d.defn_evars +let is_defined d e = EvMap.mem e d.defn_evars -let is_undefined d e = ExMap.mem e d.undf_evars +let is_undefined d e = EvMap.mem e d.undf_evars let existential_value d (n, args) = let info = find d n in @@ -321,8 +317,8 @@ let add_constraints d cstrs = (* evar_map are considered empty disregarding histories *) let is_empty d = - ExMap.is_empty d.defn_evars && - ExMap.is_empty d.undf_evars && + EvMap.is_empty d.defn_evars && + EvMap.is_empty d.undf_evars && List.is_empty d.conv_pbs && Metamap.is_empty d.metas @@ -343,31 +339,31 @@ let subst_evar_defs_light sub evd = assert (match evd.conv_pbs with [] -> true | _ -> false); let map_info i = subst_evar_info sub i in { evd with - undf_evars = ExMap.map map_info evd.undf_evars; - defn_evars = ExMap.map map_info evd.defn_evars; + undf_evars = EvMap.map map_info evd.undf_evars; + defn_evars = EvMap.map map_info evd.defn_evars; metas = Metamap.map (map_clb (subst_mps sub)) evd.metas; } let subst_evar_map = subst_evar_defs_light (* spiwack: deprecated *) let create_evar_defs sigma = { sigma with - conv_pbs=[]; last_mods=ExistentialSet.empty; metas=Metamap.empty } + conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty } (* spiwack: tentatively deprecated *) let create_goal_evar_defs sigma = { sigma with - (* conv_pbs=[]; last_mods=ExistentialSet.empty; metas=Metamap.empty } *) + (* conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty } *) metas=Metamap.empty } let empty = { - defn_evars = ExMap.empty; - undf_evars = ExMap.empty; + defn_evars = EvMap.empty; + undf_evars = EvMap.empty; universes = Univ.UniverseLSet.empty; univ_cstrs = Univ.initial_universes; conv_pbs = []; - last_mods = ExistentialSet.empty; + last_mods = Evar.Set.empty; metas = Metamap.empty; } -let has_undefined evd = not (ExMap.is_empty evd.undf_evars) +let has_undefined evd = not (EvMap.is_empty evd.undf_evars) let evars_reset_evd ?(with_conv_pbs=false) evd d = let conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs in @@ -382,23 +378,23 @@ let evar_source evk d = (find d evk).evar_source let define_aux def undef evk body = let oldinfo = - try ExMap.find evk undef + try EvMap.find evk undef with Not_found -> - if ExMap.mem evk def then + if EvMap.mem evk def then anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice") else anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar") in let () = assert (oldinfo.evar_body == Evar_empty) in let newinfo = { oldinfo with evar_body = Evar_defined body } in - ExMap.add evk newinfo def, ExMap.remove evk undef + EvMap.add evk newinfo def, EvMap.remove evk undef (* define the existential of section path sp as the constr body *) let define evk body evd = let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in let last_mods = match evd.conv_pbs with | [] -> evd.last_mods - | _ -> ExistentialSet.add evk evd.last_mods + | _ -> Evar.Set.add evk evd.last_mods in { evd with defn_evars; undf_evars; last_mods; } @@ -419,7 +415,7 @@ let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter evar_candidates = candidates; evar_extra = Store.empty; } in - { evd with undf_evars = ExMap.add evk evar_info evd.undf_evars; } + { evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; } (* extracts conversion problems that satisfy predicate p *) (* Note: conv_pbs not satisying p are stored back in reverse order *) @@ -434,7 +430,7 @@ let extract_conv_pbs evd p = ([],[]) evd.conv_pbs in - {evd with conv_pbs = pbs1; last_mods = ExistentialSet.empty}, + {evd with conv_pbs = pbs1; last_mods = Evar.Set.empty}, pbs let extract_changed_conv_pbs evd p = @@ -461,10 +457,10 @@ let evar_list evd c = let collect_evars c = let rec collrec acc c = match kind_of_term c with - | Evar (evk,_) -> ExistentialSet.add evk acc + | Evar (evk,_) -> Evar.Set.add evk acc | _ -> fold_constr collrec acc c in - collrec ExistentialSet.empty c + collrec Evar.Set.empty c (**********************************************************) (* Sort variables *) @@ -763,46 +759,46 @@ let compute_evar_dependency_graph (sigma : evar_map) = let fold evk evi acc = let fold_ev evk' acc = let tab = - try ExMap.find evk' acc - with Not_found -> ExistentialSet.empty + try EvMap.find evk' acc + with Not_found -> Evar.Set.empty in - ExMap.add evk' (ExistentialSet.add evk tab) acc + EvMap.add evk' (Evar.Set.add evk tab) acc in match evar_body evi with | Evar_empty -> assert false - | Evar_defined c -> ExistentialSet.fold fold_ev (collect_evars c) acc + | Evar_defined c -> Evar.Set.fold fold_ev (collect_evars c) acc in - ExMap.fold fold sigma.defn_evars ExMap.empty + EvMap.fold fold sigma.defn_evars EvMap.empty let evar_dependency_closure n sigma = (** Create the DAG of depth [n] representing the recursive dependencies of undefined evars. *) let graph = compute_evar_dependency_graph sigma in let rec aux n curr accu = - if Int.equal n 0 then ExistentialSet.union curr accu + if Int.equal n 0 then Evar.Set.union curr accu else let fold evk accu = try - let deps = ExMap.find evk graph in - ExistentialSet.union deps accu + let deps = EvMap.find evk graph in + Evar.Set.union deps accu with Not_found -> accu in (** Consider only the newly added evars *) - let ncurr = ExistentialSet.fold fold curr ExistentialSet.empty in + let ncurr = Evar.Set.fold fold curr Evar.Set.empty in (** Merge the others *) - let accu = ExistentialSet.union curr accu in + let accu = Evar.Set.union curr accu in aux (n - 1) ncurr accu in - let undef = ExMap.domain (undefined_map sigma) in - aux n undef ExistentialSet.empty + let undef = EvMap.domain (undefined_map sigma) in + aux n undef Evar.Set.empty let evar_dependency_closure n sigma = let deps = evar_dependency_closure n sigma in - let map = ExMap.bind (fun ev -> find sigma ev) deps in - ExMap.bindings map + let map = EvMap.bind (fun ev -> find sigma ev) deps in + EvMap.bindings map let has_no_evar sigma = - ExMap.is_empty sigma.defn_evars && ExMap.is_empty sigma.undf_evars + EvMap.is_empty sigma.defn_evars && EvMap.is_empty sigma.undf_evars let pr_evar_map_t depth sigma = let { universes = uvs; univ_cstrs = univs; } = sigma in diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 0beb46571..3d796d423 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -34,11 +34,6 @@ type evar = existential_key (** Existential variables. TODO: Should be made opaque one day. *) val string_of_existential : evar -> string -val existential_of_int : int -> evar - -module ExistentialSet : Set.S with type elt = existential_key -module ExistentialMap : Map.ExtS - with type key = existential_key and module Set := ExistentialSet (** {6 Evar infos} *) @@ -157,10 +152,10 @@ val is_undefined : evar_map -> evar -> bool val add_constraints : evar_map -> Univ.constraints -> evar_map (** Add universe constraints in an evar map. *) -val undefined_map : evar_map -> evar_info ExistentialMap.t +val undefined_map : evar_map -> evar_info Evar.Map.t (** Access the undefined evar mapping directly. *) -val defined_map : evar_map -> evar_info ExistentialMap.t +val defined_map : evar_map -> evar_info Evar.Map.t (** Access the defined evar mapping directly. *) (** {6 Instantiating partial terms} *) @@ -294,13 +289,13 @@ type evar_constraint = conv_pb * env * constr * constr val add_conv_pb : evar_constraint -> evar_map -> evar_map val extract_changed_conv_pbs : evar_map -> - (ExistentialSet.t -> evar_constraint -> bool) -> + (Evar.Set.t -> evar_constraint -> bool) -> evar_map * evar_constraint list val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t val evar_list : evar_map -> constr -> existential list -val collect_evars : constr -> ExistentialSet.t +val collect_evars : constr -> Evar.Set.t (** Metas *) val meta_list : evar_map -> (metavariable * clbinding) list diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 3623828f4..b80484599 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -32,7 +32,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with | PRef r1, PRef r2 -> eq_gr r1 r2 | PVar v1, PVar v2 -> Id.equal v1 v2 | PEvar (ev1, ctx1), PEvar (ev2, ctx2) -> - Int.equal ev1 ev2 && Array.equal constr_pattern_eq ctx1 ctx2 + Evar.equal ev1 ev2 && Array.equal constr_pattern_eq ctx1 ctx2 | PRel i1, PRel i2 -> Int.equal i1 i2 | PApp (t1, arg1), PApp (t2, arg2) -> diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 3fe2bbc12..c7c869d63 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -80,7 +80,7 @@ let evaluable_reference_eq r1 r2 = match r1, r2 with | EvalVar id1, EvalVar id2 -> Id.equal id1 id2 | EvalRel i1, EvalRel i2 -> Int.equal i1 i2 | EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) -> - Int.equal e1 e2 && Array.equal eq_constr ctx1 ctx2 + Evar.equal e1 e2 && Array.equal eq_constr ctx1 ctx2 | _ -> false let mkEvalRef = function @@ -358,7 +358,7 @@ let venv = val_of_named_context [(vfx, None, dummy); (vfun, None, dummy)] vfx (expanded fixpoint) or vfun (named function). *) let substl_with_function subst sigma constr = let evd = ref sigma in - let minargs = ref Int.Map.empty in + let minargs = ref Evar.Map.empty in let v = Array.of_list subst in let rec subst_total k c = match kind_of_term c with | Rel i when k < i -> @@ -367,7 +367,7 @@ let substl_with_function subst sigma constr = | (fx, Some (min, ref)) -> let (sigma, evk) = Evarutil.new_pure_evar !evd venv dummy in evd := sigma; - minargs := Int.Map.add evk min !minargs; + minargs := Evar.Map.add evk min !minargs; lift k (mkEvar (evk, [|fx;ref|])) | (fx, None) -> lift k fx else mkRel (i - Array.length v) @@ -387,8 +387,8 @@ let solve_arity_problem env sigma fxminargs c = let c' = whd_betaiotazeta sigma c in let (h,rcargs) = decompose_app c' in match kind_of_term h with - Evar(i,_) when Int.Map.mem i fxminargs && not (Evd.is_defined !evm i) -> - let minargs = Int.Map.find i fxminargs in + Evar(i,_) when Evar.Map.mem i fxminargs && not (Evd.is_defined !evm i) -> + let minargs = Evar.Map.find i fxminargs in if List.length rcargs < minargs then if strict then set_fix i else raise Partial; @@ -415,7 +415,7 @@ let substl_checking_arity env subst sigma c = the other ones are replaced by the function symbol *) let rec nf_fix c = match kind_of_term c with - Evar(i,[|fx;f|] as ev) when Int.Map.mem i minargs -> + Evar(i,[|fx;f|] as ev) when Evar.Map.mem i minargs -> (match Evd.existential_opt_value sigma' ev with Some c' -> c' | None -> f) diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml index 27efb9a5d..225823411 100644 --- a/pretyping/term_dnet.ml +++ b/pretyping/term_dnet.ml @@ -211,7 +211,7 @@ struct let pat_of_constr c : term_pattern = (** To each evar we associate a unique identifier. *) - let metas = ref Evd.ExistentialMap.empty in + let metas = ref Evar.Map.empty in let rec pat_of_constr c = match kind_of_term c with | Rel _ -> Term DRel | Sort _ -> Term DSort @@ -222,10 +222,10 @@ struct | Term.Meta _ -> assert false | Evar (i,_) -> let meta = - try Evd.ExistentialMap.find i !metas + try Evar.Map.find i !metas with Not_found -> let meta = fresh_meta () in - let () = metas := Evd.ExistentialMap.add i meta !metas in + let () = metas := Evar.Map.add i meta !metas in meta in Meta meta diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 9d57e1c80..81270b5f7 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -60,7 +60,7 @@ let rec pr_constr c = match kind_of_term c with (str"(" ++ pr_constr c ++ spc() ++ prlist_with_sep spc pr_constr (Array.to_list l) ++ str")") | Evar (e,l) -> hov 1 - (str"Evar#" ++ int e ++ str"{" ++ + (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++ prlist_with_sep spc pr_constr (Array.to_list l) ++str"}") | Const c -> str"Cst(" ++ pr_con c ++ str")" | Ind (sp,i) -> str"Ind(" ++ pr_mind sp ++ str"," ++ int i ++ str")" @@ -516,7 +516,7 @@ let occur_meta_or_existential c = let occur_evar n c = let rec occur_rec c = match kind_of_term c with - | Evar (sp,_) when Int.equal sp n -> raise Occur + | Evar (sp,_) when Evar.equal sp n -> raise Occur | _ -> iter_constr occur_rec c in try occur_rec c; false with Occur -> true @@ -912,18 +912,18 @@ let split_app c = match kind_of_term c with c::(Array.to_list prev), last | _ -> assert false -type subst = (rel_context*constr) Int.Map.t +type subst = (rel_context*constr) Evar.Map.t exception CannotFilter let filtering env cv_pb c1 c2 = - let evm = ref Int.Map.empty in + let evm = ref Evar.Map.empty in let define cv_pb e1 ev c1 = - try let (e2,c2) = Int.Map.find ev !evm in + try let (e2,c2) = Evar.Map.find ev !evm in let shift = List.length e1 - List.length e2 in if constr_cmp cv_pb c1 (lift shift c2) then () else raise CannotFilter with Not_found -> - evm := Int.Map.add ev (e1,c1) !evm + evm := Evar.Map.add ev (e1,c1) !evm in let rec aux env cv_pb c1 c2 = match kind_of_term c1, kind_of_term c2 with diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 92a4d961a..1aa7d9e9e 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -216,7 +216,7 @@ exception CannotFilter (context,term), or raises [CannotFilter]. Warning: Outer-kernel sort subtyping are taken into account: c1 has to be smaller than c2 wrt. sorts. *) -type subst = (rel_context*constr) Int.Map.t +type subst = (rel_context*constr) Evar.Map.t val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst val decompose_prod_letin : constr -> int * rel_context * constr diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index a1cb232ca..b5735bc64 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -506,7 +506,7 @@ let has_typeclasses filter evd = let check ev evi = filter ev (snd evi.evar_source) && is_class_evar evd evi && is_resolvable evi in - Evd.ExistentialMap.exists check (Evd.undefined_map evd) + Evar.Map.exists check (Evd.undefined_map evd) let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 14d6ad333..4f6741d87 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -228,7 +228,7 @@ type unify_flags = { (* This allows for instance to unify "forall x:A, B(x)" with "A' -> B'" *) (* This was on for all tactics, including auto, since Sep 2006 for 8.1 *) - frozen_evars : ExistentialSet.t; + frozen_evars : Evar.Set.t; (* Evars of this set are considered axioms and never instantiated *) (* Useful e.g. for autorewrite *) @@ -259,7 +259,7 @@ let default_unify_flags = { resolve_evars = false; use_pattern_unification = true; use_meta_bound_pattern_unification = true; - frozen_evars = ExistentialSet.empty; + frozen_evars = Evar.Set.empty; restrict_conv_on_strict_subterms = false; modulo_betaiota = true; modulo_eta = true; @@ -350,7 +350,7 @@ let use_full_betaiota flags = flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3 let isAllowedEvar flags c = match kind_of_term c with - | Evar (evk,_) -> not (ExistentialSet.mem evk flags.frozen_evars) + | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars) | _ -> false let check_compatibility env (sigma,metasubst,evarsubst) tyM tyN = @@ -414,13 +414,13 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag evarsubst) else error_cannot_unify_local curenv sigma (m,n,cM) | Evar (evk,_ as ev), _ - when not (ExistentialSet.mem evk flags.frozen_evars) -> + when not (Evar.Set.mem evk flags.frozen_evars) -> let cmvars = free_rels cM and cnvars = free_rels cN in if Int.Set.subset cnvars cmvars then sigma,metasubst,((curenv,ev,cN)::evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) | _, Evar (evk,_ as ev) - when not (ExistentialSet.mem evk flags.frozen_evars) -> + when not (Evar.Set.mem evk flags.frozen_evars) -> let cmvars = free_rels cM and cnvars = free_rels cN in if Int.Set.subset cmvars cnvars then sigma,metasubst,((curenv,ev,cM)::evarsubst) diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 6fbbc2c5f..5dd4587a0 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -20,7 +20,7 @@ type unify_flags = { resolve_evars : bool; use_pattern_unification : bool; use_meta_bound_pattern_unification : bool; - frozen_evars : ExistentialSet.t; + frozen_evars : Evar.Set.t; restrict_conv_on_strict_subterms : bool; modulo_betaiota : bool; modulo_eta : bool; diff --git a/printing/printer.ml b/printing/printer.ml index 70d1c9327..19dd81dcd 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -381,7 +381,7 @@ let rec pr_evars_int i = function str (string_of_existential ev) ++ str " : " ++ pegl)) ++ (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int (i+1) rest) -let pr_evars_int i evs = pr_evars_int i (Evd.ExistentialMap.bindings evs) +let pr_evars_int i evs = pr_evars_int i (Evar.Map.bindings evs) let default_pr_subgoal n sigma = let rec prrec p = function @@ -400,13 +400,13 @@ let emacs_print_dependent_evars sigma seeds = let evars () = let evars = Evarutil.gather_dependent_evars sigma seeds in let evars = - Int.Map.fold begin fun e i s -> + Evar.Map.fold begin fun e i s -> let e' = str (string_of_existential e) in match i with | None -> s ++ str" " ++ e' ++ str " open," | Some i -> s ++ str " " ++ e' ++ str " using " ++ - Int.Set.fold begin fun d s -> + Evar.Set.fold begin fun d s -> str (string_of_existential d) ++ str " " ++ s end i (str ",") end evars (str "") @@ -453,7 +453,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals = str ".") | None -> let exl = Evarutil.non_instantiated sigma in - if ExistentialMap.is_empty exl then + if Evar.Map.is_empty exl then (str"No more subgoals." ++ emacs_print_dependent_evars sigma seeds) else diff --git a/printing/printer.mli b/printing/printer.mli index 18ab975d5..8a698203a 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -129,7 +129,7 @@ val pr_concl : int -> evar_map -> goal -> std_ppcmds val pr_open_subgoals : unit -> std_ppcmds val pr_nth_open_subgoal : int -> std_ppcmds val pr_evar : (evar * evar_info) -> std_ppcmds -val pr_evars_int : int -> evar_info ExistentialMap.t -> std_ppcmds +val pr_evars_int : int -> evar_info Evar.Map.t -> std_ppcmds val pr_prim_rule : prim_rule -> std_ppcmds diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 7b1ccd542..4260d5553 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -101,7 +101,7 @@ let fail_quick_unif_flags = { resolve_evars = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; (* ? *) - frozen_evars = ExistentialSet.empty; + frozen_evars = Evar.Set.empty; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; modulo_eta = true; diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index efed7f63d..36ba80202 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -18,9 +18,9 @@ open Evarsolve (******************************************) let depends_on_evar evk _ (pbty,_,t1,t2) = - try Int.equal (head_evar t1) evk + try Evar.equal (head_evar t1) evk with NoHeadEvar -> - try Int.equal (head_evar t2) evk + try Evar.equal (head_evar t2) evk with NoHeadEvar -> false let define_and_solve_constraints evk c evd = diff --git a/proofs/goal.ml b/proofs/goal.ml index 50541151a..68eb1c586 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -27,7 +27,7 @@ type goal = { whether we do want some tags displayed besides the goal or not. *) -let pr_goal {content = e} = str "GOAL:" ++ Pp.int e +let pr_goal {content = e} = str "GOAL:" ++ Pp.int (Evar.repr e) (* access primitive *) (* invariant : [e] must exist in [em] *) @@ -41,14 +41,14 @@ let build e = } -let uid {content = e} = string_of_int e +let uid {content = e} = string_of_int (Evar.repr e) let get_by_uid u = (* this necessarily forget about tags. when tags are to be implemented, they should be done another way. We could use the store in evar_extra, for instance. *) - build (int_of_string u) + build (Evar.unsafe_of_int (int_of_string u)) (* Builds a new goal with content evar [e] and inheriting from goal [gl]*) @@ -184,7 +184,7 @@ module Refinable = struct | [] , _ -> l2 | _ , [] -> l1 | a::l1 , b::_ when a > b -> a::(fusion l1 l2) - | a::l1 , b::l2 when Int.equal a b -> a::(fusion l1 l2) + | a::l1 , b::l2 when Evar.equal a b -> a::(fusion l1 l2) | _ , b::l2 -> b::(fusion l1 l2) let update_handle handle init_defs post_defs = @@ -359,7 +359,7 @@ let plus s1 s2 env rdefs goal info = with UndefinedHere -> s2 env rdefs goal info (* Equality of two goals *) -let equal { content = e1 } { content = e2 } = Int.equal e1 e2 +let equal { content = e1 } { content = e2 } = Evar.equal e1 e2 let here goal value _ _ goal' _ = if equal goal goal' then diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 843af1373..9467d2d71 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -487,7 +487,7 @@ module V82 = struct let goals = List.map begin fun (e,_) -> Goal.build e - end (Evd.ExistentialMap.bindings undef) + end (Evar.Map.bindings undef) in { pv with comb = goals } @@ -504,14 +504,14 @@ module V82 = struct let top_evars { initial=initial } = let evars_of_initial (c,_) = - Int.Set.elements (Evarutil.evars_of_term c) + Evar.Set.elements (Evarutil.evars_of_term c) in List.flatten (List.map evars_of_initial initial) let instantiate_evar n com pv = let (evk,_) = let evl = Evarutil.non_instantiated pv.solution in - let evl = Evd.ExistentialMap.bindings evl in + let evl = Evar.Map.bindings evl in if (n <= 0) then Errors.error "incorrect existential variable index" else if List.length evl < n then diff --git a/tactics/auto.ml b/tactics/auto.ml index afb8121e8..d743135a2 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1037,7 +1037,7 @@ let auto_unif_flags = { resolve_evars = true; use_pattern_unification = false; use_meta_bound_pattern_unification = true; - frozen_evars = ExistentialSet.empty; + frozen_evars = Evar.Set.empty; restrict_conv_on_strict_subterms = false; (* Compat *) modulo_betaiota = false; modulo_eta = true; diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index c62499fdf..ee296c5e5 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -71,7 +71,7 @@ let auto_unif_flags = { resolve_evars = false; use_pattern_unification = true; use_meta_bound_pattern_unification = true; - frozen_evars = ExistentialSet.empty; + frozen_evars = Evar.Set.empty; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = true; modulo_eta = true; @@ -80,7 +80,7 @@ let auto_unif_flags = { let rec eq_constr_mod_evars x y = match kind_of_term x, kind_of_term y with - | Evar (e1, l1), Evar (e2, l2) when not (Int.equal e1 e2) -> true + | Evar (e1, l1), Evar (e2, l2) when not (Evar.equal e1 e2) -> true | _, _ -> compare_constr eq_constr_mod_evars x y let progress_evars t gl = @@ -197,7 +197,7 @@ let rec catchable = function | e -> Logic.catchable_exception e let nb_empty_evars s = - ExistentialMap.cardinal (undefined_map s) + Evar.Map.cardinal (undefined_map s) let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) (Evarutil.nf_evar evs (Goal.V82.concl evs ev)) @@ -398,7 +398,7 @@ let isProp env sigma concl = let needs_backtrack only_classes env evd oev concl = if Option.is_empty oev || isProp env evd concl then - not (Int.Set.is_empty (Evarutil.evars_of_term concl)) + not (Evar.Set.is_empty (Evarutil.evars_of_term concl)) else true let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk = @@ -525,19 +525,19 @@ let resolve_all_evars_once debug limit p evd = Beware of the imperative effects on the partition structure, it should not be shared, but only used locally. *) -module Intpart = Unionfind.Make(Int.Set)(Int.Map) +module Intpart = Unionfind.Make(Evar.Set)(Evar.Map) let deps_of_constraints cstrs evm p = List.iter (fun (_, _, x, y) -> let evx = Evarutil.undefined_evars_of_term evm x in let evy = Evarutil.undefined_evars_of_term evm y in - Intpart.union_set (Int.Set.union evx evy) p) + Intpart.union_set (Evar.Set.union evx evy) p) cstrs let evar_dependencies evm p = Evd.fold_undefined (fun ev evi _ -> - let evars = Int.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi) + let evars = Evar.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi) in Intpart.union_set evars p) evm () @@ -572,7 +572,7 @@ let split_evars evm = let evars_in_comp comp evm = try evars_reset_evd - (Int.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evm ev)) + (Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evm ev)) comp Evd.empty) evm with Not_found -> assert false @@ -590,7 +590,7 @@ let is_inference_forced p evd ev = with Not_found -> assert false let is_mandatory p comp evd = - Int.Set.exists (is_inference_forced p evd) comp + Evar.Set.exists (is_inference_forced p evd) comp (** In case of unsatisfiable constraints, build a nice error message *) @@ -630,7 +630,7 @@ let select_and_update_evars p oevd in_comp evd ev evi = let has_undefined p oevd evd = let check ev evi = snd (p oevd ev evi) in - ExistentialMap.exists check (Evd.undefined_map evd) + Evar.Map.exists check (Evd.undefined_map evd) (** Revert the resolvability status of evars after resolution, potentially unprotecting some evars that were set unresolvable @@ -655,8 +655,8 @@ let revert_resolvability oevd evd = exception Unresolved let resolve_all_evars debug m env p oevd do_split fail = - let split = if do_split then split_evars oevd else [Int.Set.empty] in - let in_comp comp ev = if do_split then Int.Set.mem ev comp else true + let split = if do_split then split_evars oevd else [Evar.Set.empty] in + let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true in let rec docomp evd = function | [] -> revert_resolvability oevd evd diff --git a/tactics/equality.ml b/tactics/equality.ml index f5ab039b4..d1d4e003d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -105,7 +105,7 @@ let rewrite_unif_flags = { Unification.resolve_evars = true; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; - Unification.frozen_evars = ExistentialSet.empty; + Unification.frozen_evars = Evar.Set.empty; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; Unification.modulo_eta = true; @@ -120,9 +120,9 @@ let freeze_initial_evars sigma flags clause = let newevars = Evd.collect_evars (clenv_type clause) in let evars = fold_undefined (fun evk _ evars -> - if ExistentialSet.mem evk newevars then evars - else ExistentialSet.add evk evars) - sigma ExistentialSet.empty in + if Evar.Set.mem evk newevars then evars + else Evar.Set.add evk evars) + sigma Evar.Set.empty in { flags with Unification.frozen_evars = evars } let make_flags frzevars sigma flags clause = @@ -178,7 +178,7 @@ let rewrite_conv_closed_unif_flags = { Unification.use_meta_bound_pattern_unification = true; - Unification.frozen_evars = ExistentialSet.empty; + Unification.frozen_evars = Evar.Set.empty; (* This is set dynamically *) Unification.restrict_conv_on_strict_subterms = false; diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 7a135bef0..fa0cb1468 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -134,7 +134,7 @@ let cstrevars evars = snd evars let new_cstr_evar (evd,cstrs) env t = let evd', t = Evarutil.new_evar evd env t in - (evd', Int.Set.add (fst (destEvar t)) cstrs), t + (evd', Evar.Set.add (fst (destEvar t)) cstrs), t let new_goal_evar (evd,cstrs) env t = let evd', t = Evarutil.new_evar evd env t in @@ -207,7 +207,7 @@ let build_signature evars env m (cstrs : (types * types option) option list) type hypinfo = { cl : clausenv; - ext : Int.Set.t; (* New evars in this clausenv *) + ext : Evar.Set.t; (* New evars in this clausenv *) prf : constr; car : constr; rel : constr; @@ -302,7 +302,7 @@ let rewrite_unif_flags = { Unification.resolve_evars = false; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; - Unification.frozen_evars = ExistentialSet.empty; + Unification.frozen_evars = Evar.Set.empty; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; Unification.modulo_eta = true; @@ -319,7 +319,7 @@ let rewrite2_unif_flags = Unification.resolve_evars = false; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; - Unification.frozen_evars = ExistentialSet.empty; + Unification.frozen_evars = Evar.Set.empty; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = true; Unification.modulo_eta = true; @@ -337,7 +337,7 @@ let general_rewrite_unif_flags () = Unification.resolve_evars = false; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; - Unification.frozen_evars = ExistentialSet.empty; + Unification.frozen_evars = Evar.Set.empty; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = true; Unification.modulo_eta = true; @@ -369,15 +369,15 @@ let solve_remaining_by by env prf = in { env with evd = evd' }, prf let extend_evd sigma ext sigma' = - Int.Set.fold (fun i acc -> + Evar.Set.fold (fun i acc -> Evd.add acc i (Evarutil.nf_evar_info sigma' (Evd.find sigma' i))) ext sigma let shrink_evd sigma ext = - Int.Set.fold (fun i acc -> Evd.remove acc i) ext sigma + Evar.Set.fold (fun i acc -> Evd.remove acc i) ext sigma let no_constraints cstrs = - fun ev _ -> not (Int.Set.mem ev cstrs) + fun ev _ -> not (Evar.Set.mem ev cstrs) let unify_eqn env (sigma, cstrs) hypinfo by t = if isEvar t then None @@ -526,7 +526,7 @@ type rewrite_flags = { under_lambdas : bool; on_morphisms : bool } let default_flags = { under_lambdas = true; on_morphisms = true; } -type evars = evar_map * Int.Set.t (* goal evars, constraint evars *) +type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *) type rewrite_proof = | RewPrf of constr * constr @@ -1129,7 +1129,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul | None -> (sort, inverse sort impl) | Some _ -> (sort, impl) in - let evars = (sigma, Int.Set.empty) in + let evars = (sigma, Evar.Set.empty) in let eq = apply_strategy strat env avoid concl (Some cstr) evars in match eq with | Some (Some (p, (evars, cstrs), car, oldt, newt)) -> @@ -1141,7 +1141,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul let evars = (* Keep only original evars (potentially instantiated) and goal evars, the rest has been defined and substituted already. *) Evd.fold (fun ev evi acc -> - if Int.Set.mem ev cstrs then Evd.remove acc ev + if Evar.Set.mem ev cstrs then Evd.remove acc ev else acc) evars' evars' in let res = @@ -1759,7 +1759,7 @@ let build_morphism_signature m = let env = Global.env () in let m = Constrintern.interp_constr Evd.empty env m in let t = Typing.type_of env Evd.empty m in - let evdref = ref (Evd.empty, Int.Set.empty) in + let evdref = ref (Evd.empty, Evar.Set.empty) in let cstrs = let rec aux t = match kind_of_term t with @@ -1790,7 +1790,7 @@ let default_morphism sign m = let env = Global.env () in let t = Typing.type_of env Evd.empty m in let evars, _, sign, cstrs = - build_signature (Evd.empty, Int.Set.empty) env t (fst sign) (snd sign) + build_signature (Evd.empty, Evar.Set.empty) env t (fst sign) (snd sign) in let morph = mkApp (Lazy.force proper_type, [| t; sign; m |]) @@ -1916,7 +1916,7 @@ let unification_rewrite flags l2r c1 c2 cl car rel but gl = check_evar_map_of_evars_defs cl'.evd; let prf = nf (Clenv.clenv_value cl') and prfty = nf (Clenv.clenv_type cl') in let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in - {cl=cl'; ext=Int.Set.empty; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; + {cl=cl'; ext=Evar.Set.empty; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty); flags = flags} let get_hyp gl evars (c,l) clause l2r = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a6826b9db..e97b01d38 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1779,8 +1779,8 @@ let default_matching_flags sigma = { use_pattern_unification = false; use_meta_bound_pattern_unification = false; frozen_evars = - fold_undefined (fun evk _ evars -> ExistentialSet.add evk evars) - sigma ExistentialSet.empty; + fold_undefined (fun evk _ evars -> Evar.Set.add evk evars) + sigma Evar.Set.empty; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; modulo_eta = false; diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 10b3febb3..73fbde781 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -43,7 +43,7 @@ let reduce x = x let rec subst_evar evar def n c = match kind_of_term c with - | Evar (e,_) when Int.equal e evar -> lift n def + | Evar (e,_) when Evar.equal e evar -> lift n def | _ -> map_constr_with_binders (fun n->n+1) (subst_evar evar def) n c let subst_evar_in_evm evar def evm = @@ -65,9 +65,9 @@ let rec safe_define evm ev c = (* msgnl(str"safe_define "++pr_evar_map evm++spc()++str" |- ?"++Pp.int ev++str" := "++pr_constr c);*) let evi = (Evd.find evm ev) in let define_subst evm sigma = - Int.Map.fold + Evar.Map.fold ( fun ev (e,c) evm -> - match kind_of_term c with Evar (i,_) when Int.equal i ev -> evm | _ -> + match kind_of_term c with Evar (i,_) when Evar.equal i ev -> evm | _ -> safe_define evm ev (lift (-List.length e) c) ) sigma evm in match evi.evar_body with @@ -95,7 +95,7 @@ let add_gen_ctx (cl,gen,evm) ctx : signature * constr list = compare function for constr instead of Pervasive's one! *) module SubstSet : Set.S with type elt = Termops.subst = Set.Make (struct type t = Termops.subst - let compare = Int.Map.compare (Pervasives.compare) + let compare = Evar.Map.compare (Pervasives.compare) (** FIXME *) end) let search_concl typ = assert false diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 1bb6f3bcf..775ffee90 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -214,7 +214,7 @@ let evars () = if s <> "" then msg_info (str s); let pfts = Proof_global.give_me_the_proof () in let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in - let exl = Evd.ExistentialMap.bindings (Evarutil.non_instantiated sigma) in + let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar ev); } in let el = List.map map_evar exl in Some el diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 0f49662c8..987c598d2 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -35,7 +35,7 @@ let succfix (depth, fixrels) = let mkMetas n = List.init n (fun _ -> Evarutil.mk_new_meta ()) let check_evars env evm = - Evd.ExistentialMap.iter + Evar.Map.iter (fun key evi -> let (loc,k) = evar_source key evm in match k with @@ -72,7 +72,7 @@ let subst_evar_constr evs n idf t = ev_hyps = hyps ; ev_chop = chop } = try evar_info k with Not_found -> - anomaly ~label:"eterm" (Pp.str "existential variable " ++ int k ++ str " not found") + anomaly ~label:"eterm" (Pp.str "existential variable " ++ int (Evar.repr k) ++ str " not found") in seen := Int.Set.add id !seen; (* Evar arguments are created in inverse order, @@ -156,54 +156,54 @@ let rec chop_product n t = | _ -> None let evars_of_evar_info evi = - Int.Set.union (Evarutil.evars_of_term evi.evar_concl) - (Int.Set.union + Evar.Set.union (Evarutil.evars_of_term evi.evar_concl) + (Evar.Set.union (match evi.evar_body with - | Evar_empty -> Int.Set.empty + | Evar_empty -> Evar.Set.empty | Evar_defined b -> Evarutil.evars_of_term b) (Evarutil.evars_of_named_context (evar_filtered_context evi))) let evar_dependencies evm oev = let one_step deps = - Int.Set.fold (fun ev s -> + Evar.Set.fold (fun ev s -> let evi = Evd.find evm ev in let deps' = evars_of_evar_info evi in - if Int.Set.mem oev deps' then - invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ string_of_int oev) - else Int.Set.union deps' s) + if Evar.Set.mem oev deps' then + invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ string_of_existential oev) + else Evar.Set.union deps' s) deps deps in let rec aux deps = let deps' = one_step deps in - if Int.Set.equal deps deps' then deps + if Evar.Set.equal deps deps' then deps else aux deps' - in aux (Int.Set.singleton oev) + in aux (Evar.Set.singleton oev) let move_after (id, ev, deps as obl) l = let rec aux restdeps = function | (id', _, _) as obl' :: tl -> - let restdeps' = Int.Set.remove id' restdeps in - if Int.Set.is_empty restdeps' then + let restdeps' = Evar.Set.remove id' restdeps in + if Evar.Set.is_empty restdeps' then obl' :: obl :: tl else obl' :: aux restdeps' tl | [] -> [obl] - in aux (Int.Set.remove id deps) l + in aux (Evar.Set.remove id deps) l let sort_dependencies evl = let rec aux l found list = match l with | (id, ev, deps) as obl :: tl -> - let found' = Int.Set.union found (Int.Set.singleton id) in - if Int.Set.subset deps found' then + let found' = Evar.Set.union found (Evar.Set.singleton id) in + if Evar.Set.subset deps found' then aux tl found' (obl :: list) else aux (move_after obl tl) found list | [] -> List.rev list - in aux evl Int.Set.empty [] + in aux evl Evar.Set.empty [] open Environ let collect_evars_of_term c ty = - Int.Set.union (Evarutil.evars_of_term c) (Evarutil.evars_of_term ty) + Evar.Set.union (Evarutil.evars_of_term c) (Evarutil.evars_of_term ty) let eterm_obligations env name evm fs ?status t ty = (* 'Serialize' the evars *) @@ -212,8 +212,8 @@ let eterm_obligations env name evm fs ?status t ty = let nc_len = Context.named_context_length nc in let evm = Evarutil.nf_evar_map_undefined evm in let evl = Evarutil.non_instantiated evm in - let evl = ExistentialMap.filter (fun ev _ -> Int.Set.mem ev evars) evl in - let evl = ExistentialMap.bindings evl in + let evl = Evar.Map.filter (fun ev _ -> Evar.Set.mem ev evars) evl in + let evl = Evar.Map.bindings evl in let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in let sevl = sort_dependencies evl in let evl = List.map (fun (id, ev, _) -> id, ev) sevl in diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index 081871fce..df9b53df5 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -33,8 +33,8 @@ val check_evars : env -> evar_map -> unit val mkMetas : int -> constr list -val evar_dependencies : evar_map -> int -> Int.Set.t -val sort_dependencies : (int * evar_info * Int.Set.t) list -> (int * evar_info * Int.Set.t) list +val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t +val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar_info * Evar.Set.t) list (* env, id, evars, number of function prototypes to try to clear from evars contexts, object and type *) |