diff options
39 files changed, 712 insertions, 628 deletions
diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4 index ebbb5505f..5b76c9587 100644 --- a/contrib/subtac/equations.ml4 +++ b/contrib/subtac/equations.ml4 @@ -880,9 +880,9 @@ let interp_pats i isevar env impls pat sign recu = str "Error parsing pattern: unnexpected left-hand side") in isevar := nf_evar_defs !isevar; - (nf_rel_context_evar (Evd.evars_of !isevar) varsctx, - nf_env_evar (Evd.evars_of !isevar) env', - rev_map (nf_evar (Evd.evars_of !isevar)) pats) + (nf_rel_context_evar ( !isevar) varsctx, + nf_env_evar ( !isevar) env', + rev_map (nf_evar ( !isevar)) pats) let interp_eqn i isevar env impls sign arity recu (pats, rhs) = let ctx, env', patcs = interp_pats i isevar env impls pats sign recu in @@ -916,8 +916,8 @@ let define_by_eqs with_comp i (l,ann) t nt eqs = let isevar = ref (create_evar_defs Evd.empty) in let (env', sign), impls = interp_context_evars isevar env l in let arity = interp_type_evars isevar env' t in - let sign = nf_rel_context_evar (Evd.evars_of !isevar) sign in - let arity = nf_evar (Evd.evars_of !isevar) arity in + let sign = nf_rel_context_evar ( !isevar) sign in + let arity = nf_evar ( !isevar) arity in let arity = if with_comp then let compid = add_suffix i "_comp" in @@ -942,11 +942,11 @@ let define_by_eqs with_comp i (l,ann) t nt eqs = Option.iter (Command.declare_interning_data data) nt; map (interp_eqn i isevar fixenv data sign arity None) eqs) () in - let sign = nf_rel_context_evar (Evd.evars_of !isevar) sign in - let arity = nf_evar (Evd.evars_of !isevar) arity in + let sign = nf_rel_context_evar ( !isevar) sign in + let arity = nf_evar ( !isevar) arity in let prob = (i, sign, arity) in - let fixenv = nf_env_evar (Evd.evars_of !isevar) fixenv in - let fixdecls = nf_rel_context_evar (Evd.evars_of !isevar) fixdecls in + let fixenv = nf_env_evar ( !isevar) fixenv in + let fixdecls = nf_rel_context_evar ( !isevar) fixdecls in (* let ce = check_evars fixenv Evd.empty !isevar in *) (* List.iter (function (_, _, Program rhs) -> ce rhs | _ -> ()) equations; *) let is_recursive, env' = @@ -966,7 +966,7 @@ let define_by_eqs with_comp i (l,ann) t nt eqs = else t, ty in let obls, t', ty' = - Eterm.eterm_obligations env i !isevar (Evd.evars_of undef) 0 ~status t ty + Eterm.eterm_obligations env i !isevar ( undef) 0 ~status t ty in if is_recursive then ignore(Subtac_obligations.add_mutual_definitions [(i, t', ty', impls, obls)] [] diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index 09ee456d7..00ed62ac8 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -310,7 +310,7 @@ let unify_tomatch_with_patterns isevars env loc typ pats = | None -> NotInd (None,typ) | Some (_,(ind,_)) -> inh_coerce_to_ind isevars env typ ind; - try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ) + try IsInd (typ,find_rectype env ( !isevars) typ) with Not_found -> NotInd (None,typ) let find_tomatch_tycon isevars env loc = function @@ -324,9 +324,9 @@ let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) = let j = typing_fun tycon env tomatch in let evd, j = Coercion.inh_coerce_to_base (loc_of_rawconstr tomatch) env !isevars j in isevars := evd; - let typ = nf_evar (Evd.evars_of !isevars) j.uj_type in + let typ = nf_evar ( !isevars) j.uj_type in let t = - try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ) + try IsInd (typ,find_rectype env ( !isevars) typ) with Not_found -> unify_tomatch_with_patterns isevars env loc typ pats in (j.uj_val,t) @@ -348,7 +348,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps) = the first pattern type and forget about the others *) let typ = match typ with IsInd (t,_) -> t | NotInd (_,t) -> t in let typ = - try IsInd (typ,find_rectype pb.env (Evd.evars_of !(pb.isevars)) typ) + try IsInd (typ,find_rectype pb.env ( !(pb.isevars)) typ) with Not_found -> NotInd (None,typ) in let tomatch = ((current,typ),deps) in match typ with @@ -366,7 +366,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps) = else (evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env) pb.isevars (make_judge current typ) (mk_tycon_type indt)).uj_val in - let sigma = Evd.evars_of !(pb.isevars) in + let sigma = !(pb.isevars) in let typ = IsInd (indt,find_rectype pb.env sigma indt) in ((current,typ),deps)) | _ -> tomatch @@ -799,7 +799,7 @@ let shift_operator k = function OpLambda _ | OpProd _ -> k+1 | _ -> k let reloc_operator (k,n) = function OpRel p when p > k -> let rec unify_clauses k pv = - let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) (Evd.evars_of isevars)) p) pv in + let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) ( isevars)) p) pv in let n1,op1 = let (n1,(op1,args1)) = pv'.(0) in n1,op1 in if Array.for_all (fun (ni,(opi,_)) -> eq_operator_lift k (n1,ni) (op1,opi)) pv' then @@ -822,7 +822,7 @@ let infer_predicate loc env isevars typs cstrs indf = (* Empiric normalization: p may depend in a irrelevant way on args of the*) (* cstr as in [c:{_:Alpha & Beta}] match c with (existS a b)=>(a,b) end *) let typs = - Array.map (local_strong whd_beta (Evd.evars_of !isevars)) typs + Array.map (local_strong whd_beta ( !isevars)) typs in let eqns = array_map2 prepare_unif_pb typs cstrs in (* First strategy: no dependencies at all *) @@ -846,7 +846,7 @@ let infer_predicate loc env isevars typs cstrs indf = (true,pred) (* true = dependent -- par défaut *) else (* - let s = get_sort_of env (evars_of isevars) typs.(0) in + let s = get_sort_of env ( isevars) typs.(0) in let predpred = it_mkLambda_or_LetIn (mkSort s) sign in let caseinfo = make_default_case_info mis in let brs = array_map2 abstract_conclusion typs cstrs in @@ -1040,11 +1040,11 @@ let find_predicate loc env isevars p typs cstrs current (IndType (indf,realargs)) tms = let (dep,pred) = match p with - | Some p -> abstract_predicate env (Evd.evars_of !isevars) indf current tms p + | Some p -> abstract_predicate env ( !isevars) indf current tms p | None -> infer_predicate loc env isevars typs cstrs indf in - let typ = whd_beta (Evd.evars_of !isevars) (applist (pred, realargs)) in + let typ = whd_beta ( !isevars) (applist (pred, realargs)) in if dep then - (pred, whd_beta (Evd.evars_of !isevars) (applist (typ, [current])), + (pred, whd_beta ( !isevars) (applist (typ, [current])), new_Type ()) else (pred, typ, new_Type ()) @@ -1271,7 +1271,7 @@ and compile_generalization pb d rest = and compile_alias pb (deppat,nondeppat,d,t) rest = let history = simplify_history pb.history in let sign, newenv, mat = - insert_aliases pb.env (Evd.evars_of !(pb.isevars)) (deppat,nondeppat,d,t) pb.mat in + insert_aliases pb.env ( !(pb.isevars)) (deppat,nondeppat,d,t) pb.mat in let n = List.length sign in (* We had Gamma1; x:current; Gamma2 |- tomatch(x) and we rebind x to get *) @@ -1427,14 +1427,14 @@ let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c = let n, allargs, env, signs = List.fold_left cook (0, [], env, []) tomatchs in let names = List.rev (List.map (List.map pi1) signs) in let allargs = - List.map (fun c -> lift n (nf_betadeltaiota env (Evd.evars_of !isevars) c)) allargs in + List.map (fun c -> lift n (nf_betadeltaiota env ( !isevars) c)) allargs in let rec build_skeleton env c = (* Don't put into normal form, it has effects on the synthesis of evars *) - (* let c = whd_betadeltaiota env (evars_of isevars) c in *) + (* let c = whd_betadeltaiota env ( isevars) c in *) (* We turn all subterms possibly dependent into an evar with maximum ctxt*) if isEvar c or List.exists (eq_constr c) allargs then e_new_evar isevars env ~src:(loc, Evd.CasesType) - (Retyping.get_type_of env (Evd.evars_of !isevars) c) + (Retyping.get_type_of env ( !isevars) c) else map_constr_with_full_binders push_rel build_skeleton env c in @@ -1595,7 +1595,7 @@ let constr_of_pat env isevars arsign pat avoid = PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid | PatCstr (l,((_, i) as cstr),args,alias) -> let cind = inductive_of_constructor cstr in - let IndType (indf, _) = find_rectype env (Evd.evars_of !isevars) (lift (-(List.length realargs)) ty) in + let IndType (indf, _) = find_rectype env ( !isevars) (lift (-(List.length realargs)) ty) in let ind, params = dest_ind_family indf in if ind <> cind then error_bad_constructor_loc l cstr ind; let cstrs = get_constructors env indf in @@ -1619,8 +1619,8 @@ let constr_of_pat env isevars arsign pat avoid = let cstr = mkConstruct ci.cs_cstr in let app = applistc cstr (List.map (lift (List.length sign)) params) in let app = applistc app args in - let apptype = Retyping.get_type_of env (Evd.evars_of !isevars) app in - let IndType (indf, realargs) = find_rectype env (Evd.evars_of !isevars) apptype in + let apptype = Retyping.get_type_of env ( !isevars) app in + let IndType (indf, realargs) = find_rectype env ( !isevars) apptype in match alias with Anonymous -> pat', sign, app, apptype, realargs, n, avoid @@ -2047,14 +2047,14 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra (* Build the dependent arity signature, the equalities which makes the first part of the predicate and their instantiations. *) let avoid = [] in - build_dependent_signature env (Evd.evars_of !isevars) avoid tomatchs arsign + build_dependent_signature env ( !isevars) avoid tomatchs arsign in let tycon, arity = match valcon_of_tycon tycon with | None -> let ev = mkExistential env isevars in ev, ev | Some t -> - t, prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars) + t, prepare_predicate_from_arsign_tycon loc env ( !isevars) tomatchs sign (lift tomatchs_len t) in let neqs, arity = diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index 15729b626..8ef215346 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -30,7 +30,7 @@ open Util module SPretyping = Subtac_pretyping.Pretyping let interp_binder_evars evdref env na t = - let t = Constrintern.intern_gen true (Evd.evars_of !evdref) env t in + let t = Constrintern.intern_gen true ( !evdref) env t in SPretyping.understand_tcc_evars evdref env IsType t let interp_binders_evars isevars env avoid l = @@ -65,7 +65,7 @@ let interp_constrs_evars isevars env avoid l = let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c = SPretyping.understand_tcc_evars evdref env kind - (intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c) + (intern_gen (kind=IsType) ~impls ( !evdref) env c) let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ = interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c @@ -94,7 +94,7 @@ let substitution_of_constrs ctx cstrs = let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) pri = let env = Global.env() in - let isevars = ref (Evd.create_evar_defs Evd.empty) in + let isevars = ref Evd.empty in let tclass = match bk with | Implicit -> @@ -134,7 +134,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p let env' = push_rel_context ctx' env in isevars := Evarutil.nf_evar_defs !isevars; isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars; - let sigma = Evd.evars_of !isevars in + let sigma = !isevars in let subst = List.map (Evarutil.nf_evar sigma) subst in let subst = let props = @@ -188,7 +188,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p Impargs.declare_manual_implicits false gr ~enriching:false imps; Typeclasses.add_instance inst in - let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in + let evm = Subtac_utils.evars_of_term ( !isevars) Evd.empty term in let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in id, Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 0af732f85..54114b0b0 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -83,7 +83,7 @@ module Coercion = struct | Type _, Prop Null -> Prop Null | _, Type _ -> s2 - let hnf env isevars c = whd_betadeltaiota env (evars_of !isevars) c + let hnf env isevars c = whd_betadeltaiota env ( !isevars) c let lift_args n sign = let rec liftrec k = function @@ -109,7 +109,7 @@ module Coercion = struct and coerce loc env isevars (x : Term.constr) (y : Term.constr) : (Term.constr -> Term.constr) option = - let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in + let x = nf_evar ( !isevars) x and y = nf_evar ( !isevars) y in let rec coerce_unify env x y = let x = hnf env isevars x and y = hnf env isevars y in try @@ -119,7 +119,7 @@ module Coercion = struct and coerce' env x y : (Term.constr -> Term.constr) option = let subco () = subset_coerce env isevars x y in let dest_prod c = - match Reductionops.splay_prod_n env (evars_of !isevars) 1 c with + match Reductionops.splay_prod_n env ( !isevars) 1 c with | [(na,b,t)], c -> (na,t), c | _ -> raise NoSubtacCoercion in @@ -209,7 +209,7 @@ module Coercion = struct isevars := evs; let (n, dom, rng) = destLambda t in let (domk, args) = destEvar dom in - isevars := evar_define domk a !isevars; + isevars := define domk a !isevars; t, rng | _ -> raise NoSubtacCoercion in @@ -252,7 +252,7 @@ module Coercion = struct end else if i = i' && len = Array.length l' then - let evm = evars_of !isevars in + let evm = !isevars in (try subco () with NoSubtacCoercion -> let typ = Typing.type_of env evm c in @@ -264,7 +264,7 @@ module Coercion = struct subco () | x, y when x = y -> if Array.length l = Array.length l' then - let evm = evars_of !isevars in + let evm = !isevars in let lam_type = Typing.type_of env evm c in let lam_type' = Typing.type_of env evm c' in (* if not (is_arity env evm lam_type) then ( *) @@ -357,7 +357,7 @@ module Coercion = struct with _ -> anomaly "apply_coercion" let inh_app_fun env isevars j = - let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in + let t = whd_betadeltaiota env ( isevars) j.uj_type in match kind_of_term t with | Prod (_,_,_) -> (isevars,j) | Evar ev when not (is_defined_evar isevars ev) -> @@ -366,8 +366,8 @@ module Coercion = struct | _ -> (try let t,p = - lookup_path_to_fun_from env (evars_of isevars) j.uj_type in - (isevars,apply_coercion env (evars_of isevars) p j t) + lookup_path_to_fun_from env ( isevars) j.uj_type in + (isevars,apply_coercion env ( isevars) p j t) with Not_found -> try let coercef, t = mu env isevars t in @@ -377,14 +377,14 @@ module Coercion = struct let inh_tosort_force loc env isevars j = try - let t,p = lookup_path_to_sort_from env (evars_of isevars) j.uj_type in - let j1 = apply_coercion env (evars_of isevars) p j t in - (isevars,type_judgment env (j_nf_evar (evars_of isevars) j1)) + let t,p = lookup_path_to_sort_from env ( isevars) j.uj_type in + let j1 = apply_coercion env ( isevars) p j t in + (isevars,type_judgment env (j_nf_evar ( isevars) j1)) with Not_found -> - error_not_a_type_loc loc env (evars_of isevars) j + error_not_a_type_loc loc env ( isevars) j let inh_coerce_to_sort loc env isevars j = - let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in + let typ = whd_betadeltaiota env ( isevars) j.uj_type in match kind_of_term typ with | Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s }) | Evar ev when not (is_defined_evar isevars ev) -> @@ -394,13 +394,13 @@ module Coercion = struct inh_tosort_force loc env isevars j let inh_coerce_to_base loc env isevars j = - let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in + let typ = whd_betadeltaiota env ( isevars) j.uj_type in let ct, typ' = mu env isevars typ in isevars, { uj_val = app_opt ct j.uj_val; uj_type = typ' } let inh_coerce_to_prod loc env isevars t = - let typ = whd_betadeltaiota env (evars_of isevars) (snd t) in + let typ = whd_betadeltaiota env ( isevars) (snd t) in let _, typ' = mu env isevars typ in isevars, (fst t, typ') @@ -411,10 +411,10 @@ module Coercion = struct else let v', t' = try - let t2,t1,p = lookup_path_between env (evars_of evd) (t,c1) in + let t2,t1,p = lookup_path_between env ( evd) (t,c1) in match v with Some v -> - let j = apply_coercion env (evars_of evd) p + let j = apply_coercion env ( evd) p {uj_val = v; uj_type = t} t2 in Some j.uj_val, j.uj_type | None -> None, t @@ -430,8 +430,8 @@ module Coercion = struct try inh_coerce_to_fail env evd rigidonly v t c1 with NoCoercion -> match - kind_of_term (whd_betadeltaiota env (evars_of evd) t), - kind_of_term (whd_betadeltaiota env (evars_of evd) c1) + kind_of_term (whd_betadeltaiota env ( evd) t), + kind_of_term (whd_betadeltaiota env ( evd) c1) with | Prod (name,t1,t2), Prod (_,u1,u2) -> (* Conversion did not work, we may succeed with a coercion. *) @@ -463,7 +463,7 @@ module Coercion = struct (Some (nf_isevar evd cj.uj_val)) (nf_isevar evd cj.uj_type) (nf_isevar evd t) with NoCoercion -> - let sigma = evars_of evd in + let sigma = evd in try coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t with NoSubtacCoercion -> @@ -484,7 +484,7 @@ module Coercion = struct | Some (init, cur) -> init, cur in try - let rels, rng = Reductionops.splay_prod_n env (evars_of isevars) nabs t in + let rels, rng = Reductionops.splay_prod_n env ( isevars) nabs t in (* The final range free variables must have been replaced by evars, we accept only that evars in rng are applied to free vars. *) if noccur_with_meta 1 (succ nabs) rng then ( @@ -497,7 +497,7 @@ module Coercion = struct with NoCoercion -> coerce_itf loc env' isevars None t t') with NoSubtacCoercion -> - let sigma = evars_of isevars in + let sigma = isevars in error_cannot_coerce env' sigma (t, t')) else isevars with _ -> isevars diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 4876b0655..674805962 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -57,7 +57,7 @@ let evar_nf isevars c = let interp_gen kind isevars env ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) c = - let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars (Evd.evars_of !isevars) env c in + let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in evar_nf isevars c' @@ -75,14 +75,14 @@ let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ = let interp_open_constr isevars env c = msgnl (str "Pretyping " ++ my_print_constr_expr c); - let c = Constrintern.intern_constr (Evd.evars_of !isevars) env c in + let c = Constrintern.intern_constr ( !isevars) env c in let c' = SPretyping.pretype_gen isevars env ([], []) (OfType None) c in evar_nf isevars c' let interp_constr_judgment isevars env c = let j = SPretyping.understand_judgment_tcc isevars env - (Constrintern.intern_constr (Evd.evars_of !isevars) env c) + (Constrintern.intern_constr ( !isevars) env c) in { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type } @@ -95,11 +95,11 @@ let locate_if_isevar loc na = function | x -> x let interp_binder sigma env na t = - let t = Constrintern.intern_gen true (Evd.evars_of !sigma) env t in + let t = Constrintern.intern_gen true ( !sigma) env t in SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t) let interp_context_evars evdref env params = - let bl = Constrintern.intern_context false (Evd.evars_of !evdref) env params in + let bl = Constrintern.intern_context false ( !evdref) env params in let (env, par, _, impls) = List.fold_left (fun (env,params,n,impls) (na, k, b, t) -> @@ -299,8 +299,8 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let typ = it_mkProd_or_LetIn top_arity binders_rel in let fullcoqc = Evarutil.nf_isevar !isevars def in let fullctyp = Evarutil.nf_isevar !isevars typ in - let evm = evars_of_term (Evd.evars_of !isevars) Evd.empty fullctyp in - let evm = evars_of_term (Evd.evars_of !isevars) evm fullcoqc in + let evm =evars_of_term ( !isevars) Evd.empty fullctyp in + let evm = evars_of_term ( !isevars) evm fullcoqc in let evm = non_instanciated_map env isevars evm in let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in Subtac_obligations.add_definition recname evars_def evars_typ ~implicits:impls evars @@ -351,7 +351,7 @@ let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype = let push_named_context = List.fold_right push_named let check_evars env initial_sigma evd c = - let sigma = evars_of evd in + let sigma = evd in let c = nf_evar sigma c in let rec proc_rec c = match kind_of_term c with @@ -374,7 +374,7 @@ let interp_recursive fixkind l boxed = let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in (* Interp arities allowing for unresolved types *) - let evdref = ref (Evd.create_evar_defs Evd.empty) in + let evdref = ref Evd.empty in let fixctxs, fiximps = List.split (List.map (interp_fix_context evdref env) fixl) in let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in let fixtypes = List.map2 build_fix_type fixctxs fixccls in @@ -397,9 +397,9 @@ let interp_recursive fixkind l boxed = (* Instantiate evars and check all are resolved *) let evd,_ = Evarconv.consider_remaining_unif_problems env_rec !evdref in - let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in - let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in - let rec_sign = nf_named_context_evar (evars_of evd) rec_sign in + let fixdefs = List.map (nf_evar ( evd)) fixdefs in + let fixtypes = List.map (nf_evar ( evd)) fixtypes in + let rec_sign = nf_named_context_evar ( evd) rec_sign in let recdefs = List.length rec_sign in List.iter (check_evars env_rec Evd.empty evd) fixdefs; @@ -410,7 +410,7 @@ let interp_recursive fixkind l boxed = (* Get the interesting evars, those that were not instanciated *) let isevars = Evd.undefined_evars evd in - let evm = Evd.evars_of isevars in + let evm = isevars in (* Solve remaining evars *) let rec collect_evars id def typ imps = (* Generalize by the recursive prototypes *) diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index 0159de542..d9df5b34c 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -74,7 +74,7 @@ let interp env isevars c tycon = let evd,_ = consider_remaining_unif_problems env !isevars in (* let unevd = undefined_evars evd in *) let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in - let evm = evars_of unevd' in + let evm = unevd' in isevars := unevd'; nf_evar evm j.uj_val, nf_evar evm j.uj_type @@ -86,8 +86,8 @@ let find_with_index x l = open Vernacexpr -let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env -let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type (evars_of evd) env +let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr ( evd) env +let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type ( evd) env let env_with_binders env isevars l = let rec aux ((env, rels) as acc) = function @@ -123,7 +123,7 @@ let subtac_process env isevars id bl c tycon = let c = coqintern_constr !isevars env c in let imps = Implicit_quantifiers.implicits_of_rawterm c in let coqc, ctyp = interp env isevars c tycon in - let evm = non_instanciated_map env isevars (evars_of !isevars) in + let evm = non_instanciated_map env isevars ( !isevars) in let ty = nf_isevar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in evm, coqc, ty, imps diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 023213ecb..01fe4ef6f 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -79,14 +79,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct for i = 0 to lt-1 do if not (e_cumul env isevars (vdefj.(i)).uj_type (lift lt lar.(i))) then - error_ill_typed_rec_body_loc loc env (evars_of !isevars) + error_ill_typed_rec_body_loc loc env ( !isevars) i lna vdefj lar done let check_branches_message loc env isevars c (explft,lft) = for i = 0 to Array.length explft - 1 do if not (e_cumul env isevars lft.(i) explft.(i)) then - let sigma = evars_of !isevars in + let sigma = !isevars in error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i) done @@ -99,7 +99,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (* let evar_type_case isevars env ct pt lft p c = - let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c + let (mind,bty,rslty) = type_case_branches env ( isevars) ct pt p c in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty) *) @@ -158,7 +158,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | RType _ -> judge_of_new_Type () (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *) - (* in environment [env], with existential variables [(evars_of isevars)] and *) + (* in environment [env], with existential variables [( isevars)] and *) (* the type constraint tycon *) let rec pretype (tycon : type_constraint) env isevars lvar c = (* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ *) @@ -179,12 +179,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | REvar (loc, ev, instopt) -> (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) - let hyps = evar_context (Evd.find (evars_of !isevars) ev) in + let hyps = evar_context (Evd.find ( !isevars) ev) in let args = match instopt with | None -> instance_from_named_context hyps | Some inst -> failwith "Evar subtitutions not implemented" in let c = mkEvar (ev, args) in - let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in + let j = (Retyping.get_judgment_of env ( !isevars) c) in inh_conv_coerce_to_tycon loc env isevars j tycon | RPatVar (loc,(someta,n)) -> @@ -246,8 +246,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in evar_type_fixpoint loc env isevars names ftys vdefj; - let ftys = Array.map (nf_evar (evars_of !isevars)) ftys in - let fdefs = Array.map (fun x -> nf_evar (evars_of !isevars) (j_val x)) vdefj in + let ftys = Array.map (nf_evar ( !isevars)) ftys in + let fdefs = Array.map (fun x -> nf_evar ( !isevars) (j_val x)) vdefj in let fixj = match fixkind with | RFix (vn,i) -> (* First, let's find the guard indexes. *) @@ -297,7 +297,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | c::rest -> let argloc = loc_of_rawconstr c in let resj = evd_comb1 (Coercion.inh_app_fun env) isevars resj in - let resty = whd_betadeltaiota env (evars_of !isevars) resj.uj_type in + let resty = whd_betadeltaiota env ( !isevars) resj.uj_type in match kind_of_term resty with | Prod (na,c1,c2) -> Option.iter (fun ty -> isevars := @@ -315,14 +315,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | _ -> let hj = pretype empty_tycon env isevars lvar c in error_cant_apply_not_functional_loc - (join_loc floc argloc) env (evars_of !isevars) + (join_loc floc argloc) env ( !isevars) resj [hj] in - let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in + let resj = j_nf_evar ( !isevars) (apply_rec env 1 fj ftycon args) in let resj = match kind_of_term resj.uj_val with | App (f,args) when isInd f or isConst f -> - let sigma = evars_of !isevars in + let sigma = !isevars in let c = mkApp (f,Array.map (whd_evar sigma) args) in let t = Retyping.get_type_of env sigma c in make_judge c t @@ -369,10 +369,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | RLetTuple (loc,nal,(na,po),c,d) -> let cj = pretype empty_tycon env isevars lvar c in let (IndType (indf,realargs)) = - try find_rectype env (evars_of !isevars) cj.uj_type + try find_rectype env ( !isevars) cj.uj_type with Not_found -> let cloc = loc_of_rawconstr c in - error_case_not_inductive_loc cloc env (evars_of !isevars) cj + error_case_not_inductive_loc cloc env ( !isevars) cj in let cstrs = get_constructors env indf in if Array.length cstrs <> 1 then @@ -396,14 +396,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | Some p -> let env_p = push_rels psign env in let pj = pretype_type empty_valcon env_p isevars lvar p in - let ccl = nf_evar (evars_of !isevars) pj.utj_val in + let ccl = nf_evar ( !isevars) pj.utj_val in let psign = make_arity_signature env true indf in (* with names *) let p = it_mkLambda_or_LetIn ccl psign in let inst = (Array.to_list cs.cs_concl_realargs) @[build_dependent_constructor cs] in let lp = lift cs.cs_nargs p in - let fty = hnf_lam_applist env (evars_of !isevars) lp inst in + let fty = hnf_lam_applist env ( !isevars) lp inst in let fj = pretype (mk_tycon fty) env_f isevars lvar d in let f = it_mkLambda_or_LetIn fj.uj_val fsign in let v = @@ -416,12 +416,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let tycon = lift_tycon cs.cs_nargs tycon in let fj = pretype tycon env_f isevars lvar d in let f = it_mkLambda_or_LetIn fj.uj_val fsign in - let ccl = nf_evar (evars_of !isevars) fj.uj_type in + let ccl = nf_evar ( !isevars) fj.uj_type in let ccl = if noccur_between 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl else - error_cant_find_case_type_loc loc env (evars_of !isevars) + error_cant_find_case_type_loc loc env ( !isevars) cj.uj_val in let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in let v = @@ -434,10 +434,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | RIf (loc,c,(na,po),b1,b2) -> let cj = pretype empty_tycon env isevars lvar c in let (IndType (indf,realargs)) = - try find_rectype env (evars_of !isevars) cj.uj_type + try find_rectype env ( !isevars) cj.uj_type with Not_found -> let cloc = loc_of_rawconstr c in - error_case_not_inductive_loc cloc env (evars_of !isevars) cj in + error_case_not_inductive_loc cloc env ( !isevars) cj in let cstrs = get_constructors env indf in if Array.length cstrs <> 2 then user_err_loc (loc,"", @@ -456,7 +456,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | Some p -> let env_p = push_rels psign env in let pj = pretype_type empty_valcon env_p isevars lvar p in - let ccl = nf_evar (evars_of !isevars) pj.utj_val in + let ccl = nf_evar ( !isevars) pj.utj_val in let pred = it_mkLambda_or_LetIn ccl psign in let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in let jtyp = inh_conv_coerce_to_tycon loc env isevars {uj_val = pred; @@ -470,8 +470,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in - let pred = nf_evar (evars_of !isevars) pred in - let p = nf_evar (evars_of !isevars) p in + let pred = nf_evar ( !isevars) pred in + let p = nf_evar ( !isevars) p in (* msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*) let f cs b = let n = rel_context_length cs.cs_args in @@ -525,7 +525,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | RDynamic (loc,d) -> if (tag d) = "constr" then let c = constr_out d in - let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in + let j = (Retyping.get_judgment_of env ( !isevars) c) in j (*inh_conv_coerce_to_tycon loc env isevars j tycon*) else @@ -537,7 +537,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (match valcon with | Some v -> let s = - let sigma = evars_of !isevars in + let sigma = !isevars in let t = Retyping.get_type_of env sigma v in match kind_of_term (whd_betadeltaiota env sigma t) with | Sort s -> s @@ -561,7 +561,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct if e_cumul env isevars v tj.utj_val then tj else error_unexpected_type_loc - (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v + (loc_of_rawconstr c) env ( !isevars) tj.utj_val v let pretype_gen_aux isevars env lvar kind c = let c' = match kind with @@ -572,12 +572,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (pretype_type empty_valcon env isevars lvar c).utj_val in let evd,_ = consider_remaining_unif_problems env !isevars in isevars:=evd; - nf_evar (evars_of !isevars) c' + nf_evar ( !isevars) c' let pretype_gen isevars env lvar kind c = let c = pretype_gen_aux isevars env lvar kind c in isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !isevars; - nf_evar (evars_of !isevars) c + nf_evar ( !isevars) c (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage @@ -587,14 +587,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let understand_judgment sigma env c = let isevars = ref (create_evar_defs sigma) in let j = pretype empty_tycon env isevars ([],[]) c in - let j = j_nf_evar (evars_of !isevars) j in + let j = j_nf_evar ( !isevars) j in let isevars,_ = consider_remaining_unif_problems env !isevars in check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j let understand_judgment_tcc isevars env c = let j = pretype empty_tycon env isevars ([],[]) c in - let sigma = evars_of !isevars in + let sigma = !isevars in let j = j_nf_evar sigma j in j @@ -635,7 +635,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let c = pretype_gen_aux isevars env ([],[]) (OfType exptyp) c in !isevars, c in - Evd.evars_of ev, t + ev, t end module Default : S = SubtacPretyping_F(Coercion.Default) diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index cdbc40232..ba30ee190 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -437,7 +437,7 @@ let pr_evar_info evi = in hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]") -let pr_evar_map sigma = +let pr_evar_defs sigma = h 0 (prlist_with_sep pr_fnl (fun (ev,evi) -> @@ -455,9 +455,9 @@ let pr_constraints pbs = let pr_evar_defs evd = let pp_evm = - let evars = evars_of evd in + let evars = evd in if evars = empty then mt() else - str"EVARS:"++brk(0,1)++pr_evar_map evars++fnl() in + str"EVARS:"++brk(0,1)++pr_evar_defs evars++fnl() in let pp_met = if meta_list evd = [] then mt() else str"METAS:"++brk(0,1)++pr_meta_map evd in diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml index 30dc7b710..f7524671f 100644 --- a/contrib/xml/proof2aproof.ml +++ b/contrib/xml/proof2aproof.ml @@ -149,7 +149,7 @@ let extract_open_proof sigma pf = in let unsharedconstr = let evar_nf_constr = - nf_evar (Evd.evars_of !evd) + nf_evar ( !evd) ~preserve:(function e -> S.mem e !unshared_constrs) constr in Unshare.unshare @@ -159,14 +159,14 @@ let extract_open_proof sigma pf = (*CSC: debugging stuff to be removed *) if ProofTreeHash.mem proof_tree_to_constr node then Pp.ppnl (Pp.(++) (Pp.str "#DUPLICATE INSERTION: ") - (Tactic_printer.print_proof (Evd.evars_of !evd) [] node)) ; + (Tactic_printer.print_proof ( !evd) [] node)) ; ProofTreeHash.add proof_tree_to_constr node unsharedconstr ; unshared_constrs := S.add unsharedconstr !unshared_constrs ; unsharedconstr in let unshared_pf = unshare_proof_tree pf in let pfterm = proof_extractor [] unshared_pf in - (pfterm, Evd.evars_of !evd, proof_tree_to_constr, proof_tree_to_flattened_proof_tree, + (pfterm, !evd, proof_tree_to_constr, proof_tree_to_flattened_proof_tree, unshared_pf) ;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index d7d2f6d8e..5e3fbb616 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -99,16 +99,16 @@ let pp_transparent_state s = pp (pr_transparent_state s) (* proof printers *) let ppmetas metas = pp(pr_metaset metas) -let ppevm evd = pp(pr_evar_map evd) +let ppevm evd = pp(pr_evar_defs evd) let ppevd evd = pp(pr_evar_defs evd) let ppclenv clenv = pp(pr_clenv clenv) let ppgoal g = pp(db_pr_goal g) let pr_gls gls = - hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) + hov 0 (pr_evar_defs (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) let pr_glls glls = - hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++ + hov 0 (pr_evar_defs (sig_sig glls) ++ fnl () ++ prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) let ppsigmagoal g = pp(pr_goal (sig_it g)) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 87768c419..a447fbe8d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1255,7 +1255,7 @@ let interp_open_constr_patvar sigma env c = ) | _ -> map_rawconstr patvar_to_evar r in let raw = patvar_to_evar raw in - Default.understand_tcc (Evd.evars_of !sigma) env raw + Default.understand_tcc ( !sigma) env raw let interp_constr_judgment sigma env c = Default.understand_judgment sigma env (intern_constr sigma env c) @@ -1268,12 +1268,12 @@ let interp_constr_evars_gen_impls ?evdref let imps = Implicit_quantifiers.implicits_of_rawterm c in Default.understand_gen kind Evd.empty env c, imps | Some evdref -> - let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in + let c = intern_gen (kind=IsType) ~impls ( !evdref) env c in let imps = Implicit_quantifiers.implicits_of_rawterm c in Default.understand_tcc_evars evdref env kind c, imps let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c = - let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in + let c = intern_gen (kind=IsType) ~impls ( !evdref) env c in Default.understand_tcc_evars evdref env kind c let interp_casted_constr_evars_impls ?evdref @@ -1294,7 +1294,7 @@ let interp_type_evars evdref env ?(impls=([],[])) c = let interp_constr_judgment_evars evdref env c = Default.understand_judgment_tcc evdref env - (intern_constr (Evd.evars_of !evdref) env c) + (intern_constr ( !evdref) env c) type ltac_sign = identifier list * unbound_ltac_var_map @@ -1324,7 +1324,7 @@ let interp_binder sigma env na t = Default.understand_type sigma env t' let interp_binder_evars evdref env na t = - let t = intern_gen true (Evd.evars_of !evdref) env t in + let t = intern_gen true ( !evdref) env t in let t' = locate_if_isevar (loc_of_rawconstr t) na t in Default.understand_tcc_evars evdref env IsType t' @@ -1371,7 +1371,7 @@ let interp_context ?(fail_anonymous=false) sigma env params = (Default.understand_judgment sigma) env bl let interp_context_evars ?(fail_anonymous=false) evdref env params = - let bl = intern_context fail_anonymous (Evd.evars_of !evdref) env params in + let bl = intern_context fail_anonymous ( !evdref) env params in interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t) (Default.understand_judgment_tcc evdref) env bl diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index d48c85616..a9d370447 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -149,7 +149,7 @@ let free_vars_of_rawconstr ?(bound=Idset.empty) = let rec make_fresh ids env x = if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_ident x) -let freevars_of_ids env ids = +let fre_ids env ids = List.filter (is_freevar env (Global.env())) ids let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id diff --git a/pretyping/cases.ml b/pretyping/cases.ml index dcedfa51d..8451d1285 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -363,7 +363,7 @@ let unify_tomatch_with_patterns evdref env loc typ pats realnames = | None -> NotInd (None,typ) | Some (_,(ind,_)) -> inh_coerce_to_ind evdref env typ ind; - try try_find_ind env (evars_of !evdref) typ realnames + try try_find_ind env ( !evdref) typ realnames with Not_found -> NotInd (None,typ) let find_tomatch_tycon evdref env loc = function @@ -377,9 +377,9 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) = let loc = Some (loc_of_rawconstr tomatch) in let tycon,realnames = find_tomatch_tycon evdref env loc indopt in let j = typing_fun tycon env evdref tomatch in - let typ = nf_evar (evars_of !evdref) j.uj_type in + let typ = nf_evar ( !evdref) j.uj_type in let t = - try try_find_ind env (evars_of !evdref) typ realnames + try try_find_ind env ( !evdref) typ realnames with Not_found -> unify_tomatch_with_patterns evdref env loc typ pats realnames in (j.uj_val,t) @@ -414,7 +414,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = let typ,names = match typ with IsInd(t,_,names) -> t,Some names | NotInd(_,t) -> t,None in let typ = - try try_find_ind pb.env (evars_of !(pb.evdref)) typ names + try try_find_ind pb.env ( !(pb.evdref)) typ names with Not_found -> NotInd (None,typ) in let tomatch = ((current,typ),deps,dep) in match typ with @@ -432,7 +432,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = else (evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env) pb.evdref (make_judge current typ) (mk_tycon_type indt)).uj_val in - let sigma = evars_of !(pb.evdref) in + let sigma = !(pb.evdref) in let typ = try_find_ind pb.env sigma indt names in ((current,typ),deps,dep)) | _ -> tomatch @@ -934,10 +934,10 @@ let expand_arg tms ccl ((_,t),_,na) = let adjust_impossible_cases pb pred tomatch submat = if submat = [] then - match kind_of_term (whd_evar (evars_of !(pb.evdref)) pred) with + match kind_of_term (whd_evar ( !(pb.evdref)) pred) with | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) = ImpossibleCase -> let default = (coq_unit_judge ()).uj_type in - pb.evdref := Evd.evar_define evk default !(pb.evdref); + pb.evdref := Evd.define evk default !(pb.evdref); (* we add an "assert false" case *) let pats = List.map (fun _ -> PatVar (dummy_loc,Anonymous)) tomatch in let aliasnames = @@ -989,8 +989,8 @@ let specialize_predicate newtomatchs (names,(depna,_)) cs tms ccl = List.fold_left (expand_arg tms) ccl''' newtomatchs let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms = - let pred= abstract_predicate env (evars_of !evdref) indf current dep tms p in - (pred, whd_betaiota (evars_of !evdref) + let pred= abstract_predicate env ( !evdref) indf current dep tms p in + (pred, whd_betaiota ( !evdref) (applist (pred, realargs@[current])), new_Type ()) let adjust_predicate_from_tomatch ((_,oldtyp),_,(nadep,_)) typ pb = @@ -1068,7 +1068,7 @@ let rec generalize_problem names pb = function let build_leaf pb = let rhs = extract_rhs pb in let j = pb.typing_function (mk_tycon pb.pred) rhs.rhs_env pb.evdref rhs.it in - j_nf_evar (evars_of !(pb.evdref)) j + j_nf_evar ( !(pb.evdref)) j (* Building the sub-problem when all patterns are variables *) let shift_problem ((current,t),_,(nadep,_)) pb = @@ -1236,7 +1236,7 @@ and compile_generalization pb d rest = and compile_alias pb (deppat,nondeppat,d,t) rest = let history = simplify_history pb.history in let sign, newenv, mat = - insert_aliases pb.env (evars_of !(pb.evdref)) (deppat,nondeppat,d,t) pb.mat in + insert_aliases pb.env ( !(pb.evdref)) (deppat,nondeppat,d,t) pb.mat in let n = List.length sign in (* We had Gamma1; x:current; Gamma2 |- tomatch(x) and we rebind x to get *) @@ -1456,7 +1456,7 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t = *) let abstract_tycon loc env evdref subst _tycon extenv t = - let sigma = evars_of !evdref in + let sigma = !evdref in let t = nf_betaiota sigma t in (* it helps in some cases to remove K-redex *) let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv subst t in (* We traverse the type T of the original problem Xi looking for subterms @@ -1503,7 +1503,7 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t = e_new_evar evdref env ~src:(loc,ImpossibleCase) (new_Type ()) in lift (n'-n) impossible_case_type | Some t -> abstract_tycon loc tycon_env evdref subst tycon extenv t in - get_judgment_of extenv (evars_of !evdref) t + get_judgment_of extenv ( !evdref) t (* For a multiple pattern-matching problem Xi on t1..tn with return * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return @@ -1516,7 +1516,7 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t = *) let build_inversion_problem loc env evdref tms t = - let sigma = evars_of !evdref in + let sigma = !evdref in let make_patvar t (subst,avoid) = let id = next_name_away (named_hd env t Anonymous) avoid in PatVar (dummy_loc,Name id), ((id,t)::subst, id::avoid) in diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 24f3b7726..05c64521a 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -45,7 +45,7 @@ type clausenv = { templtyp : constr freelisted } let cl_env ce = ce.env -let cl_sigma ce = evars_of ce.evd +let cl_sigma ce = ce.evd let subst_clenv sub clenv = { templval = map_fl (subst_mps sub) clenv.templval; @@ -129,7 +129,7 @@ let clenv_conv_leq env sigma t c bound = let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in let evars,_ = Evarconv.consider_remaining_unif_problems env evars in - let args = List.map (whd_evar (Evd.evars_of evars)) args in + let args = List.map (whd_evar ( evars)) args in check_evars env sigma evars (applist (c,args)); args @@ -254,7 +254,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags) clenv = { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd } let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl = - if isMeta (fst (whd_stack (evars_of clenv.evd) clenv.templtyp.rebus)) then + if isMeta (fst (whd_stack ( clenv.evd) clenv.templtyp.rebus)) then clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) (pf_concl gl) (clenv_unify_meta_types ~flags:flags clenv) else @@ -341,7 +341,7 @@ let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv { templval = clenv.templval; templtyp = clenv.templtyp; evd = - evar_merge (meta_merge clenv.evd nextclenv.evd) (evars_of clenv.evd); + evar_merge (meta_merge clenv.evd nextclenv.evd) ( clenv.evd); env = nextclenv.env } in (* unify the type of the template of [nextclenv] with the type of [mv] *) let clenv'' = @@ -402,7 +402,7 @@ let error_already_defined b = (str "Position " ++ int n ++ str" already defined.") let clenv_unify_binding_type clenv c t u = - if isMeta (fst (whd_stack (evars_of clenv.evd) u)) then + if isMeta (fst (whd_stack ( clenv.evd) u)) then (* Not enough information to know if some subtyping is needed *) CoerceToType, clenv, c else @@ -416,7 +416,7 @@ let clenv_unify_binding_type clenv c t u = let clenv_assign_binding clenv k (sigma,c) = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in - let c_typ = nf_betaiota (evars_of clenv'.evd) (clenv_get_type_of clenv' c) in + let c_typ = nf_betaiota ( clenv'.evd) (clenv_get_type_of clenv' c) in let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd } diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 85e14d482..3a5f35125 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -123,7 +123,7 @@ module Default = struct with _ -> anomaly "apply_coercion" let inh_app_fun env evd j = - let t = whd_betadeltaiota env (evars_of evd) j.uj_type in + let t = whd_betadeltaiota env ( evd) j.uj_type in match kind_of_term t with | Prod (_,_,_) -> (evd,j) | Evar ev -> @@ -132,21 +132,21 @@ module Default = struct | _ -> (try let t,p = - lookup_path_to_fun_from env (evars_of evd) j.uj_type in - (evd,apply_coercion env (evars_of evd) p j t) + lookup_path_to_fun_from env ( evd) j.uj_type in + (evd,apply_coercion env ( evd) p j t) with Not_found -> (evd,j)) let inh_tosort_force loc env evd j = try - let t,p = lookup_path_to_sort_from env (evars_of evd) j.uj_type in - let j1 = apply_coercion env (evars_of evd) p j t in - let j2 = on_judgment_type (whd_evar (evars_of evd)) j1 in + let t,p = lookup_path_to_sort_from env ( evd) j.uj_type in + let j1 = apply_coercion env ( evd) p j t in + let j2 = on_judgment_type (whd_evar ( evd)) j1 in (evd,type_judgment env j2) with Not_found -> - error_not_a_type_loc loc env (evars_of evd) j + error_not_a_type_loc loc env ( evd) j let inh_coerce_to_sort loc env evd j = - let typ = whd_betadeltaiota env (evars_of evd) j.uj_type in + let typ = whd_betadeltaiota env ( evd) j.uj_type in match kind_of_term typ with | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s }) | Evar ev when not (is_defined_evar evd ev) -> @@ -166,11 +166,11 @@ module Default = struct else let v', t' = try - let t2,t1,p = lookup_path_between env (evars_of evd) (t,c1) in + let t2,t1,p = lookup_path_between env ( evd) (t,c1) in match v with Some v -> let j = - apply_coercion env (evars_of evd) p + apply_coercion env ( evd) p {uj_val = v; uj_type = t} t2 in Some j.uj_val, j.uj_type | None -> None, t @@ -185,8 +185,8 @@ module Default = struct try inh_coerce_to_fail env evd rigidonly v t c1 with NoCoercion -> match - kind_of_term (whd_betadeltaiota env (evars_of evd) t), - kind_of_term (whd_betadeltaiota env (evars_of evd) c1) + kind_of_term (whd_betadeltaiota env ( evd) t), + kind_of_term (whd_betadeltaiota env ( evd) c1) with | Prod (name,t1,t2), Prod (_,u1,u2) -> (* Conversion did not work, we may succeed with a coercion. *) @@ -215,7 +215,7 @@ module Default = struct try inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercion -> - let sigma = evars_of evd in + let sigma = evd in error_actual_type_loc loc env sigma cj t in let val' = match val' with Some v -> v | None -> assert(false) in @@ -253,7 +253,7 @@ module Default = struct pi1 (inh_conv_coerce_to_fail loc env' evd None t t') with NoCoercion -> evd) (* Maybe not enough information to unify *) - (*let sigma = evars_of evd in + (*let sigma = evd in error_cannot_coerce env' sigma (t, t'))*) else evd with Invalid_argument _ -> evd *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d7da100ab..d185bd64e 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -52,7 +52,7 @@ let eval_flexible_term env c = | _ -> assert false let evar_apprec env evd stack c = - let sigma = evars_of evd in + let sigma = evd in let rec aux s = let (t,stack) = whd_betaiota_deltazeta_for_iota_state env sigma s in match kind_of_term t with @@ -62,7 +62,7 @@ let evar_apprec env evd stack c = in aux (c, append_stack_list stack empty_stack) let apprec_nohdbeta env evd c = - match kind_of_term (fst (Reductionops.whd_stack (evars_of evd) c)) with + match kind_of_term (fst (Reductionops.whd_stack ( evd) c)) with | (Case _ | Fix _) -> applist (evar_apprec env evd [] c) | _ -> c @@ -158,7 +158,7 @@ let ise_array2 evd f v1 v2 = else (evd,false) let rec evar_conv_x env evd pbty term1 term2 = - let sigma = evars_of evd in + let sigma = evd in let term1 = whd_castappevar sigma term1 in let term2 = whd_castappevar sigma term2 in (* Maybe convertible but since reducing can erase evars which [evar_apprec] @@ -166,7 +166,7 @@ let rec evar_conv_x env evd pbty term1 term2 = Note: incomplete heuristic... *) let ground_test = if is_ground_term evd term1 && is_ground_term evd term2 then - if is_fconv pbty env (evars_of evd) term1 term2 then + if is_fconv pbty env ( evd) term1 term2 then Some true else if is_ground_env evd env then Some false else None @@ -222,7 +222,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = then (* Miller-Pfenning's patterns unification *) (* Preserve generality (except that CCI has no eta-conversion) *) - let t2 = nf_evar (evars_of evd) (applist appr2) in + let t2 = nf_evar ( evd) (applist appr2) in let t2 = solve_pattern_eqn env l1 t2 in solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2) else if @@ -254,7 +254,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = then (* Miller-Pfenning's patterns unification *) (* Preserve generality (except that CCI has no eta-conversion) *) - let t1 = nf_evar (evars_of evd) (applist appr1) in + let t1 = nf_evar ( evd) (applist appr1) in let t1 = solve_pattern_eqn env l2 t1 in solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1) else if @@ -293,7 +293,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = if the first argument is a beta-redex (expand a constant only if necessary) or the second argument is potentially usable as a canonical projection *) - if isLambda flex1 or is_open_canonical_projection (evars_of i) appr2 + if isLambda flex1 or is_open_canonical_projection ( i) appr2 then match eval_flexible_term env flex1 with | Some v1 -> @@ -322,7 +322,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = then (* Miller-Pfenning's patterns unification *) (* Preserve generality (except that CCI has no eta-conversion) *) - let t2 = nf_evar (evars_of evd) (applist appr2) in + let t2 = nf_evar ( evd) (applist appr2) in let t2 = solve_pattern_eqn env l1 t2 in solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2) else @@ -337,7 +337,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = then (* Miller-Pfenning's patterns unification *) (* Preserve generality (except that CCI has no eta-conversion) *) - let t1 = nf_evar (evars_of evd) (applist appr1) in + let t1 = nf_evar ( evd) (applist appr1) in let t1 = solve_pattern_eqn env l2 t1 in solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1) else @@ -382,7 +382,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = ise_and evd [(fun i -> evar_conv_x env i CONV c1 c2); (fun i -> - let c = nf_evar (evars_of i) c1 in + let c = nf_evar ( i) c1 in evar_conv_x (push_rel (na,None,c) env) i CONV c'1 c'2)] | LetIn (na,b1,t1,c'1), LetIn (_,b2,_,c'2) -> @@ -390,8 +390,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = ise_and i [(fun i -> evar_conv_x env i CONV b1 b2); (fun i -> - let b = nf_evar (evars_of i) b1 in - let t = nf_evar (evars_of i) t1 in + let b = nf_evar ( i) b1 in + let t = nf_evar ( i) t1 in evar_conv_x (push_rel (na,Some b,t) env) i pbty c'1 c'2); (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2)] @@ -414,7 +414,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = ise_and evd [(fun i -> evar_conv_x env i CONV c1 c2); (fun i -> - let c = nf_evar (evars_of i) c1 in + let c = nf_evar ( i) c1 in evar_conv_x (push_rel (n,None,c) env) i pbty c'1 c'2)] | Ind sp1, Ind sp2 -> @@ -508,15 +508,15 @@ let first_order_unification env evd (ev1,l1) (term2,l2) = solve_simple_eqn evar_conv_x env i (CONV,ev1,t2))] let choose_less_dependent_instance evk evd term args = - let evi = Evd.find (evars_of evd) evk in + let evi = Evd.find ( evd) evk in let subst = make_pure_subst evi args in let subst' = List.filter (fun (id,c) -> c = term) subst in if subst' = [] then error "Too complex unification problem." else - Evd.evar_define evk (mkVar (fst (List.hd subst'))) evd + Evd.define evk (mkVar (fst (List.hd subst'))) evd let apply_conversion_problem_heuristic env evd pbty t1 t2 = - let t1 = apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t1) in - let t2 = apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t2) in + let t1 = apprec_nohdbeta env evd (whd_castappevar ( evd) t1) in + let t2 = apprec_nohdbeta env evd (whd_castappevar ( evd) t2) in let (term1,l1 as appr1) = decompose_app t1 in let (term2,l2 as appr2) = decompose_app t2 in match kind_of_term term1, kind_of_term term2 with diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 37288d394..0ef2c6319 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -79,13 +79,13 @@ let nf_evar_info evc info = let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi)) evm Evd.empty -let nf_evar_defs evd = Evd.evars_reset_evd (nf_evars (Evd.evars_of evd)) evd +let nf_evar_defs evd = Evd.evars_reset_evd (nf_evars ( evd)) evd -let nf_isevar evd = nf_evar (Evd.evars_of evd) -let j_nf_isevar evd = j_nf_evar (Evd.evars_of evd) -let jl_nf_isevar evd = jl_nf_evar (Evd.evars_of evd) -let jv_nf_isevar evd = jv_nf_evar (Evd.evars_of evd) -let tj_nf_isevar evd = tj_nf_evar (Evd.evars_of evd) +let nf_isevar evd = nf_evar ( evd) +let j_nf_isevar evd = j_nf_evar ( evd) +let jl_nf_isevar evd = jl_nf_evar ( evd) +let jv_nf_isevar evd = jv_nf_evar ( evd) +let tj_nf_isevar evd = tj_nf_evar ( evd) (**********************) (* Creating new metas *) @@ -279,7 +279,7 @@ let evar_well_typed_body evd ev evi body = try let env = evar_unfiltered_env evi in let ty = evi.evar_concl in - Typing.check env (evars_of evd) body ty; + Typing.check env ( evd) body ty; true with e -> pperrnl @@ -339,13 +339,13 @@ let shrink_context env subst ty = shrink_named subst [] rev_named_sign let extend_evar env evdref k (evk1,args1) c = - let ty = get_type_of env (evars_of !evdref) c in + let ty = get_type_of env ( !evdref) c in let overwrite_first v1 v2 = let v = Array.copy v1 in let n = Array.length v - Array.length v2 in for i = 0 to Array.length v2 - 1 do v.(n+i) <- v2.(i) done; v in - let evi1 = Evd.find (evars_of !evdref) evk1 in + let evi1 = Evd.find ( !evdref) evk1 in let named_sign',rel_sign',ty = if k = 0 then [], [], ty else shrink_context env (List.rev (make_pure_subst evi1 args1)) ty in @@ -378,7 +378,7 @@ let restrict_upon_filter evd evi evk p args = if newfilter <> filter then let (evd,newev) = new_evar evd (evar_unfiltered_env evi) ~src:(evar_source evk evd) ~filter:newfilter evi.evar_concl in - let evd = Evd.evar_define evk newev evd in + let evd = Evd.define evk newev evd in evd,fst (destEvar newev),newargs else evd,evk,args @@ -416,7 +416,7 @@ let rec check_and_clear_in_constr evdref err ids c = | Evar (evk,l as ev) -> if Evd.is_defined_evar !evdref ev then (* If evk is already defined we replace it by its definition *) - let nc = whd_evar (evars_of !evdref) c in + let nc = whd_evar ( !evdref) c in (check_and_clear_in_constr evdref err ids nc) else (* We check for dependencies to elements of ids in the @@ -424,7 +424,7 @@ let rec check_and_clear_in_constr evdref err ids c = arguments. Concurrently, we build a new evar corresponding to e where hypotheses of ids have been removed *) - let evi = Evd.find (evars_of !evdref) evk in + let evi = Evd.find ( !evdref) evk in let ctxt = Evd.evar_filtered_context evi in let (nhyps,nargs,rids) = List.fold_right2 @@ -455,7 +455,7 @@ let rec check_and_clear_in_constr evdref err ids c = let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in - evdref := Evd.evar_define evk ev' !evdref; + evdref := Evd.define evk ev' !evdref; let (evk',_) = destEvar ev' in mkEvar(evk', Array.of_list nargs) @@ -605,17 +605,17 @@ let project_with_effects env sigma effects t subst = * type is an evar too. * * Note: typing creates new evar problems, which induces a recursive dependency - * with [evar_define]. To avoid a too large set of recursive functions, we - * pass [evar_define] to [do_projection_effects] as a parameter. + * with [define]. To avoid a too large set of recursive functions, we + * pass [define] to [do_projection_effects] as a parameter. *) let rec do_projection_effects define_fun env ty evd = function | ProjectVar -> evd | ProjectEvar ((evk,argsv),evi,id,p) -> - let evd = Evd.evar_define evk (mkVar id) evd in + let evd = Evd.define evk (mkVar id) evd in (* TODO: simplify constraints involving evk *) let evd = do_projection_effects define_fun env ty evd p in - let ty = whd_betadeltaiota env (evars_of evd) (Lazy.force ty) in + let ty = whd_betadeltaiota env ( evd) (Lazy.force ty) in if not (isSort ty) then (* Don't try to instantiate if a sort because if evar_concl is an evar it may commit to a univ level which is not the right @@ -623,7 +623,7 @@ let rec do_projection_effects define_fun env ty evd = function unif, we know that no coercion can be inserted) *) let subst = make_pure_subst evi argsv in let ty' = replace_vars subst evi.evar_concl in - let ty' = whd_evar (evars_of evd) ty' in + let ty' = whd_evar ( evd) ty' in if isEvar ty' then define_fun env (destEvar ty') ty evd else evd else evd @@ -682,7 +682,7 @@ let effective_projections = map_succeed (function Invertible c -> c | _ -> failwith"") let instance_of_projection f env t evd projs = - let ty = lazy (Retyping.get_type_of env (evars_of evd) t) in + let ty = lazy (Retyping.get_type_of env ( evd) t) in match projs with | NoUniqueProjection -> raise NotUnique | UniqueProjection (c,effects) -> @@ -719,7 +719,7 @@ let do_restrict_hyps_virtual evd evk filter = interest for this early detection in practice is not obvious. We let it for future work. In any case, thanks to the use of filters, the whole (unrestricted) context remains consistent. *) - let evi = Evd.find (evars_of evd) evk in + let evi = Evd.find ( evd) evk in let env = evar_unfiltered_env evi in let oldfilter = evar_filter evi in let filter,_ = List.fold_right (fun oldb (l,filter) -> @@ -734,7 +734,7 @@ let do_restrict_hyps evd evk projs = evd,evk else let evd,nc = do_restrict_hyps_virtual evd evk filter in - let evd = Evd.evar_define evk nc evd in + let evd = Evd.define evk nc evd in let evk',_ = destEvar nc in evd,evk' @@ -742,7 +742,7 @@ let do_restrict_hyps evd evk projs = let postpone_evar_term env evd (evk,argsv) rhs = let rhs = expand_vars_in_term env rhs in - let evi = Evd.find (evars_of evd) evk in + let evi = Evd.find ( evd) evk in let evd,evk,args = restrict_upon_filter evd evi evk (* Keep only variables that depends in rhs *) @@ -789,14 +789,14 @@ let postpone_evar_evar env evd projs1 (evk1,args1) projs2 (evk2,args2) = exception CannotProject of projectibility_status list let solve_evar_evar_l2r f env evd (evk1,args1) (evk2,_ as ev2) = - let proj1 = array_map_to_list (invert_arg env 0 (evars_of evd) ev2) args1 in + let proj1 = array_map_to_list (invert_arg env 0 ( evd) ev2) args1 in try (* Instantiate ev2 with (a restriction of) ev1 if uniquely projectable *) let proj1' = effective_projections proj1 in let evd,args1' = list_fold_map (instance_of_projection f env (mkEvar ev2)) evd proj1' in let evd,evk1' = do_restrict_hyps evd evk1 proj1 in - Evd.evar_define evk2 (mkEvar(evk1',Array.of_list args1')) evd + Evd.define evk2 (mkEvar(evk1',Array.of_list args1')) evd with NotUnique -> raise (CannotProject proj1) @@ -842,16 +842,16 @@ exception NotEnoughInformationToProgress let rec invert_definition env evd (evk,argsv as ev) rhs = let evdref = ref evd in let progress = ref false in - let evi = Evd.find (evars_of evd) evk in - let subst = make_projectable_subst (evars_of evd) evi argsv in + let evi = Evd.find ( evd) evk in + let subst = make_projectable_subst ( evd) evi argsv in (* Projection *) let project_variable t = (* Evar/Var problem: unifiable iff variable projectable from ev subst *) try - let sols = find_projectable_vars true env (evars_of !evdref) t subst in + let sols = find_projectable_vars true env ( !evdref) t subst in let c, p = filter_solution sols in - let ty = lazy (Retyping.get_type_of env (evars_of !evdref) t) in + let ty = lazy (Retyping.get_type_of env ( !evdref) t) in let evd = do_projection_effects evar_define env ty !evdref p in evdref := evd; c @@ -871,16 +871,16 @@ let rec invert_definition env evd (evk,argsv as ev) rhs = evar in let rec imitate (env',k as envk) t = - let t = whd_evar (evars_of !evdref) t in + let t = whd_evar ( !evdref) t in match kind_of_term t with | Rel i when i>k -> project_variable (mkRel (i-k)) | Var id -> project_variable t | Evar (evk',args' as ev') -> - if evk = evk' then error_occur_check env (evars_of evd) evk rhs; + if evk = evk' then error_occur_check env ( evd) evk rhs; (* Evar/Evar problem (but left evar is virtual) *) let projs' = array_map_to_list - (invert_arg_from_subst env k (evars_of !evdref) subst) args' + (invert_arg_from_subst env k ( !evdref) subst) args' in (try (* Try to project (a restriction of) the right evar *) @@ -909,13 +909,13 @@ let rec invert_definition env evd (evk,argsv as ev) rhs = map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1) imitate envk t in - let rhs = whd_beta (evars_of evd) rhs (* heuristic *) in + let rhs = whd_beta ( evd) rhs (* heuristic *) in let body = imitate (env,0) rhs in (!evdref,body) -(* [evar_define] tries to solve the problem "?ev[args] = rhs" when "?ev" is +(* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said, - * [evar_define] tries to find an instance lhs such that + * [define] tries to find an instance lhs such that * "lhs [hyps:=args]" unifies to rhs. The term "lhs" must be closed in * context "hyps" and not referring to itself. *) @@ -932,7 +932,7 @@ and evar_define env (evk,_ as ev) rhs evd = if occur_meta body then error "Meta cannot occur in evar body."; (* invert_definition may have instantiate some evars of rhs with evk *) (* so we recheck acyclicity *) - if occur_evar evk body then error_occur_check env (evars_of evd) evk body; + if occur_evar evk body then error_occur_check env ( evd) evk body; (* needed only if an inferred type *) let body = refresh_universes body in (* Cannot strictly type instantiations since the unification algorithm @@ -943,7 +943,7 @@ and evar_define env (evk,_ as ev) rhs evd = try let env = evar_env evi in let ty = evi.evar_concl in - Typing.check env (evars_of evd') body ty + Typing.check env ( evd') body ty with e -> pperrnl (str "Ill-typed evar instantiation: " ++ fnl() ++ @@ -951,19 +951,19 @@ and evar_define env (evk,_ as ev) rhs evd = str "----> " ++ int ev ++ str " := " ++ print_constr body); raise e in*) - Evd.evar_define evk body evd' + Evd.define evk body evd' with | NotEnoughInformationToProgress -> postpone_evar_term env evd ev rhs | NotInvertibleUsingOurAlgorithm t -> - error_not_clean env (evars_of evd) evk t (evar_source evk evd) + error_not_clean env ( evd) evk t (evar_source evk evd) (*-------------------*) (* Auxiliary functions for the conversion algorithms modulo evars *) let has_undefined_evars evd t = - let evm = evars_of evd in + let evm = evd in let rec has_ev t = match kind_of_term t with Evar (ev,args) -> @@ -1079,7 +1079,7 @@ let solve_pattern_eqn env l1 c = * hyps of the existential, to do a "pop" for each Rel which is * not an argument of the existential, and a subst1 for each which * is, again, with the corresponding variable. This is done by - * evar_define + * define * * Thus, we take the arguments of the existential which we are about * to assign, and zip them with the identifiers in the hypotheses. @@ -1105,7 +1105,7 @@ let status_changed lev (pbty,_,t1,t2) = let solve_refl conv_algo env evd evk argsv1 argsv2 = if argsv1 = argsv2 then evd else - let evi = Evd.find (evars_of evd) evk in + let evi = Evd.find ( evd) evk in (* Filter and restrict if needed *) let evd,evk,args = restrict_upon_filter evd evi evk @@ -1125,7 +1125,7 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 = (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *) let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) = try - let t2 = whd_evar (evars_of evd) t2 in + let t2 = whd_evar ( evd) t2 in let evd = match kind_of_term t2 with | Evar (evk2,args2 as ev2) -> if evk1 = evk2 then @@ -1136,7 +1136,7 @@ let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) = else add_conv_pb (pbty,env,mkEvar ev1,t2) evd | _ -> let evd = evar_define env ev1 t2 evd in - let evm = evars_of evd in + let evm = evd in let evi = Evd.find evm evk1 in if occur_existential evm evi.evar_concl then let evenv = evar_env evi in @@ -1180,7 +1180,7 @@ let evars_of_evar_info evi = (* it assumes that the defined existentials have already been substituted *) let check_evars env initial_sigma evd c = - let sigma = evars_of evd in + let sigma = evd in let c = nf_evar sigma c in let rec proc_rec c = match kind_of_term c with @@ -1238,7 +1238,7 @@ let mk_valcon c = Some c cumulativity now includes Prop and Set in Type... It is, but that's not too bad *) let define_evar_as_abstraction abs evd (ev,args) = - let evi = Evd.find (evars_of evd) ev in + let evi = Evd.find ( evd) ev in let evenv = evar_unfiltered_env evi in let (evd1,dom) = new_evar evd evenv (new_Type()) ~filter:(evar_filter evi) in let nvar = @@ -1249,7 +1249,7 @@ let define_evar_as_abstraction abs evd (ev,args) = new_evar evd1 newenv ~src:(evar_source ev evd1) (new_Type()) ~filter:(true::evar_filter evi) in let prod = abs (Name nvar, dom, subst_var nvar rng) in - let evd3 = Evd.evar_define ev prod evd2 in + let evd3 = Evd.define ev prod evd2 in let evdom = fst (destEvar dom), args in let evrng = fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in @@ -1264,7 +1264,7 @@ let define_evar_as_lambda evd (ev,args) = let define_evar_as_sort evd (ev,args) = let s = new_Type () in - Evd.evar_define ev s evd, destSort s + Evd.define ev s evd, destSort s (* We don't try to guess in which sort the type should be defined, since @@ -1279,7 +1279,7 @@ let judge_of_new_Type () = Typeops.judge_of_type (new_univ ()) let split_tycon loc env evd tycon = let rec real_split c = - let sigma = evars_of evd in + let sigma = evd in let t = whd_betadeltaiota env sigma c in match kind_of_term t with | Prod (na,dom,rng) -> evd, (na, dom, rng) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 400ad2f7a..9ee34b40d 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -23,6 +23,9 @@ open Mod_subst type evar = existential_key +let string_of_existential evk = "?" ^ string_of_int evk +let existential_of_int evk = evk + type evar_body = | Evar_empty | Evar_defined of constr @@ -60,97 +63,107 @@ let eq_evar_info ei1 ei2 = eq_named_context_val (ei1.evar_hyps) (ei2.evar_hyps) && ei1.evar_body = ei2.evar_body -module Evarmap = Intmap - -type evar_map1 = evar_info Evarmap.t - -let empty = Evarmap.empty - -let to_list evc = (* Workaround for change in Map.fold behavior *) - let l = ref [] in - Evarmap.iter (fun evk x -> l := (evk,x)::!l) evc; - !l - -let dom evc = Evarmap.fold (fun evk _ acc -> evk::acc) evc [] -let find evc k = Evarmap.find k evc -let remove evc k = Evarmap.remove k evc -let mem evc k = Evarmap.mem k evc -let fold = Evarmap.fold - -let add evd evk newinfo = Evarmap.add evk newinfo evd - -let define evd evk body = - let oldinfo = - try find evd evk - with Not_found -> error "Evd.define: cannot define undeclared evar" in - let newinfo = - { oldinfo with - evar_body = Evar_defined body } in - match oldinfo.evar_body with - | Evar_empty -> Evarmap.add evk newinfo evd - | _ -> anomaly "Evd.define: cannot define an evar twice" - -let is_evar sigma evk = mem sigma evk - -let is_defined sigma evk = - let info = find sigma evk in - not (info.evar_body = Evar_empty) - -let string_of_existential evk = "?" ^ string_of_int evk - -let existential_of_int evk = evk - -(*******************************************************************) -(* Formerly Instantiate module *) - -let is_id_inst inst = - let is_id (id,c) = match kind_of_term c with - | Var id' -> id = id' - | _ -> false - in - List.for_all is_id inst - -(* VĂ©rifier que les instances des let-in sont compatibles ?? *) -let instantiate_sign_including_let sign args = - let rec instrec = function - | ((id,b,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args)) - | ([],[]) -> [] - | ([],_) | (_,[]) -> - anomaly "Signature and its instance do not match" - in - instrec (sign,args) - -let instantiate_evar sign c args = - let inst = instantiate_sign_including_let sign args in - if is_id_inst inst then - c - else - replace_vars inst c - -(* Existentials. *) +(* spiwack: Revised hierarchy : + - ExistentialMap ( Maps of existential_keys ) + - EvarInfoMap ( .t = evar_info ExistentialMap.t ) + - EvarMap ( .t = EvarInfoMap.t * sort_constraints ) + - evar_defs (exported) +*) -let existential_type sigma (n,args) = - let info = - try find sigma n - with Not_found -> - anomaly ("Evar "^(string_of_existential n)^" was not declared") in - let hyps = evar_filtered_context info in - instantiate_evar hyps info.evar_concl (Array.to_list args) +module ExistentialMap = Intmap +(* This exception is raised by *.existential_value *) exception NotInstantiatedEvar -let existential_value sigma (n,args) = - let info = find sigma n in - let hyps = evar_filtered_context info in - match evar_body info with - | Evar_defined c -> - instantiate_evar hyps c (Array.to_list args) - | Evar_empty -> - raise NotInstantiatedEvar +module EvarInfoMap = struct + type t = evar_info ExistentialMap.t + + let empty = ExistentialMap.empty + + let to_list evc = (* Workaround for change in Map.fold behavior *) + let l = ref [] in + ExistentialMap.iter (fun evk x -> l := (evk,x)::!l) evc; + !l + + let dom evc = ExistentialMap.fold (fun evk _ acc -> evk::acc) evc [] + let find evc k = ExistentialMap.find k evc + let remove evc k = ExistentialMap.remove k evc + let mem evc k = ExistentialMap.mem k evc + let fold = ExistentialMap.fold + + let add evd evk newinfo = ExistentialMap.add evk newinfo evd + + let equal = ExistentialMap.equal + + let define evd evk body = + let oldinfo = + try find evd evk + with Not_found -> error "Evd.define: cannot define undeclared evar" in + let newinfo = + { oldinfo with + evar_body = Evar_defined body } in + match oldinfo.evar_body with + | Evar_empty -> ExistentialMap.add evk newinfo evd + | _ -> anomaly "Evd.define: cannot define an evar twice" + + let is_evar sigma evk = mem sigma evk + + let is_defined sigma evk = + let info = find sigma evk in + not (info.evar_body = Evar_empty) + + + (*******************************************************************) + (* Formerly Instantiate module *) + + let is_id_inst inst = + let is_id (id,c) = match kind_of_term c with + | Var id' -> id = id' + | _ -> false + in + List.for_all is_id inst + + (* VĂ©rifier que les instances des let-in sont compatibles ?? *) + let instantiate_sign_including_let sign args = + let rec instrec = function + | ((id,b,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args)) + | ([],[]) -> [] + | ([],_) | (_,[]) -> + anomaly "Signature and its instance do not match" + in + instrec (sign,args) + + let instantiate_evar sign c args = + let inst = instantiate_sign_including_let sign args in + if is_id_inst inst then + c + else + replace_vars inst c + + (* Existentials. *) + + let existential_type sigma (n,args) = + let info = + try find sigma n + with Not_found -> + anomaly ("Evar "^(string_of_existential n)^" was not declared") in + let hyps = evar_filtered_context info in + instantiate_evar hyps info.evar_concl (Array.to_list args) + + let existential_value sigma (n,args) = + let info = find sigma n in + let hyps = evar_filtered_context info in + match evar_body info with + | Evar_defined c -> + instantiate_evar hyps c (Array.to_list args) + | Evar_empty -> + raise NotInstantiatedEvar + + let existential_opt_value sigma ev = + try Some (existential_value sigma ev) + with NotInstantiatedEvar -> None -let existential_opt_value sigma ev = - try Some (existential_value sigma ev) - with NotInstantiatedEvar -> None +end (*******************************************************************) (* Constraints for sort variables *) @@ -285,39 +298,29 @@ let pr_sort_cstrs g = hov 0 (prlist_with_sep spc Univ.pr_uni leq) ++ str"]") l -type evar_map = evar_map1 * sort_constraints -let empty = empty, UniverseMap.empty -let add (sigma,sm) k v = (add sigma k v, sm) -let dom (sigma,_) = dom sigma -let find (sigma,_) = find sigma -let remove (sigma,sm) k = (remove sigma k, sm) -let mem (sigma,_) = mem sigma -let to_list (sigma,_) = to_list sigma -let fold f (sigma,_) = fold f sigma -let define (sigma,sm) k v = (define sigma k v, sm) -let is_evar (sigma,_) = is_evar sigma -let is_defined (sigma,_) = is_defined sigma -let existential_value (sigma,_) = existential_value sigma -let existential_type (sigma,_) = existential_type sigma -let existential_opt_value (sigma,_) = existential_opt_value sigma -let eq_evar_map x y = x == y || - (Evarmap.equal eq_evar_info (fst x) (fst y) && +module EvarMap = struct + type t = EvarInfoMap.t * sort_constraints + let empty = EvarInfoMap.empty, UniverseMap.empty + let add (sigma,sm) k v = (EvarInfoMap.add sigma k v, sm) + let dom (sigma,_) = EvarInfoMap.dom sigma + let find (sigma,_) = EvarInfoMap.find sigma + let remove (sigma,sm) k = (EvarInfoMap.remove sigma k, sm) + let mem (sigma,_) = EvarInfoMap.mem sigma + let to_list (sigma,_) = EvarInfoMap.to_list sigma + let fold f (sigma,_) = EvarInfoMap.fold f sigma + let define (sigma,sm) k v = (EvarInfoMap.define sigma k v, sm) + let is_evar (sigma,_) = EvarInfoMap.is_evar sigma + let is_defined (sigma,_) = EvarInfoMap.is_defined sigma + let existential_value (sigma,_) = EvarInfoMap.existential_value sigma + let existential_type (sigma,_) = EvarInfoMap.existential_type sigma + let existential_opt_value (sigma,_) = EvarInfoMap.existential_opt_value sigma + let eq_evar_map x y = x == y || + (EvarInfoMap.equal eq_evar_info (fst x) (fst y) && UniverseMap.equal (=) (snd x) (snd y)) -let merge e e' = fold (fun n v sigma -> add sigma n v) e' e - -(*******************************************************************) -type open_constr = evar_map * constr - -(*******************************************************************) -(* The type constructor ['a sigma] adds an evar map to an object of - type ['a] *) -type 'a sigma = { - it : 'a ; - sigma : evar_map} - -let sig_it x = x.it -let sig_sig x = x.sigma + let merge e e' = fold (fun n v sigma -> add sigma n v) e' e + +end (*******************************************************************) (* Metamaps *) @@ -418,12 +421,55 @@ type hole_kind = type conv_pb = Reduction.conv_pb type evar_constraint = conv_pb * Environ.env * constr * constr type evar_defs = - { evars : evar_map; + { evars : EvarMap.t; conv_pbs : evar_constraint list; last_mods : existential_key list; history : (existential_key * (loc * hole_kind)) list; metas : clbinding Metamap.t } +(*** Lifting primitive from EvarMap. ***) +type evar_map = evar_defs +(* spiwack: this function seems to be used only for the definition of the progress + tactical. I would recommand not using it in other places. *) +let eq_evar_map d1 d2 = + EvarMap.eq_evar_map d1.evars d2.evars + +(* spiwack: tentative. It might very well not be the semantics we want + for merging evar_defs *) +let merge d1 d2 = { +(* d1 with evars = EvarMap.merge d1.evars d2.evars*) + evars = EvarMap.merge d1.evars d2.evars ; + conv_pbs = List.rev_append d1.conv_pbs d2.conv_pbs ; + last_mods = List.rev_append d1.last_mods d2.last_mods ; + history = List.rev_append d1.history d2.history ; + metas = Metamap.fold (fun k m r -> Metamap.add k m r) d2.metas d1.metas +} +let add d e i = { d with evars=EvarMap.add d.evars e i } +let remove d e = { d with evars=EvarMap.remove d.evars e } +let dom d = EvarMap.dom d.evars +let find d e = EvarMap.find d.evars e +let mem d e = EvarMap.mem d.evars e +(* spiwack: this function loses information from the original evar_defs + it might be an idea not to export it. *) +let to_list d = EvarMap.to_list d.evars +(* spiwack: not clear what folding over an evar_defs, for now we shall + simply fold over the inner evar_map. *) +let fold f d a = EvarMap.fold f d.evars a +let is_evar d e = EvarMap.is_evar d.evars e +let is_defined d e = EvarMap.is_defined d.evars e + +let existential_value d e = EvarMap.existential_value d.evars e +let existential_type d e = EvarMap.existential_type d.evars e +let existential_opt_value d e = EvarMap.existential_opt_value d.evars e + +(*** /Lifting... ***) + +(* evar_defs are considered empty disregarding histories *) +let is_empty d = + d.evars = EvarMap.empty && + d.conv_pbs = [] && + Metamap.is_empty d.metas + let subst_named_context_val s = map_named_val (subst_mps s) let subst_evar_info s evi = @@ -434,36 +480,40 @@ let subst_evar_info s evi = evar_hyps = subst_named_context_val s evi.evar_hyps; evar_body = subst_evb evi.evar_body } -let subst_evar_map sub evm = - assert (snd evm = UniverseMap.empty); - Evarmap.map (subst_evar_info sub) (fst evm), snd evm - let subst_evar_defs_light sub evd = - assert (snd evd.evars = UniverseMap.empty); + assert (UniverseMap.is_empty (snd evd.evars)); assert (evd.conv_pbs = []); { evd with metas = Metamap.map (map_clb (subst_mps sub)) evd.metas; - evars = Evarmap.map (subst_evar_info sub) (fst evd.evars), snd evd.evars + evars = ExistentialMap.map (subst_evar_info sub) (fst evd.evars), snd evd.evars } -let create_evar_defs sigma = - { evars=sigma; conv_pbs=[]; last_mods = []; history=[]; metas=Metamap.empty } -let create_goal_evar_defs sigma = - let h = fold (fun mv _ l -> (mv,(dummy_loc,GoalEvar))::l) sigma [] in - { evars=sigma; conv_pbs=[]; last_mods = []; history=h; metas=Metamap.empty } -let empty_evar_defs = create_evar_defs empty -let evars_of d = d.evars -let evars_reset_evd evd d = {d with evars = evd} -let reset_evd (sigma,mmap) d = {d with evars = sigma; metas=mmap} +let subst_evar_map = subst_evar_defs_light + +(* spiwack: deprecated *) +let create_evar_defs sigma = { sigma with + conv_pbs=[]; last_mods=[]; history=[]; metas=Metamap.empty } +(* spiwack: tentatively deprecated *) +let create_goal_evar_defs sigma = { sigma with + conv_pbs=[]; last_mods=[]; metas=Metamap.empty } +let empty = { + evars=EvarMap.empty; + conv_pbs=[]; + last_mods = []; + history=[]; + metas=Metamap.empty +} + +let evars_reset_evd evd d = {d with evars = evd.evars} let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs} let evar_source evk d = try List.assoc evk d.history with Not_found -> (dummy_loc, InternalHole) (* define the existential of section path sp as the constr body *) -let evar_define evk body evd = +let define evk body evd = { evd with - evars = define evd.evars evk body; + evars = EvarMap.define evd.evars evk body; last_mods = evk :: evd.last_mods } let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd = @@ -476,7 +526,7 @@ let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd = filter) in { evd with - evars = add evd.evars evk + evars = EvarMap.add evd.evars evk {evar_hyps = hyps; evar_concl = ty; evar_body = Evar_empty; @@ -484,7 +534,7 @@ let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd = evar_extra = None}; history = (evk,src)::evd.history } -let is_defined_evar evd (evk,_) = is_defined evd.evars evk +let is_defined_evar evd (evk,_) = EvarMap.is_defined evd.evars evk (* Does k corresponds to an (un)defined existential ? *) let is_undefined_evar evd c = match kind_of_term c with @@ -493,9 +543,9 @@ let is_undefined_evar evd c = match kind_of_term c with let undefined_evars evd = let evars = - fold (fun evk evi sigma -> if evi.evar_body = Evar_empty then - add sigma evk evi else sigma) - evd.evars empty + EvarMap.fold (fun evk evi sigma -> if evi.evar_body = Evar_empty then + EvarMap.add sigma evk evi else sigma) + evd.evars EvarMap.empty in { evd with evars = evars } @@ -521,23 +571,24 @@ let extract_changed_conv_pbs evd p = let extract_all_conv_pbs evd = extract_conv_pbs evd (fun _ -> true) +(* spiwack: should it be replaced by Evd.merge? *) let evar_merge evd evars = - { evd with evars = merge evd.evars evars } + { evd with evars = EvarMap.merge evd.evars evars.evars } (**********************************************************) (* Sort variables *) -let new_sort_variable (sigma,sm) = +let new_sort_variable ({ evars = (sigma,sm) } as d)= let (u,scstr) = new_sort_var sm in - (Type u,(sigma,scstr)) -let is_sort_variable (_,sm) s = + (Type u,{ d with evars = (sigma,scstr) } ) +let is_sort_variable {evars=(_,sm)} s = is_sort_var s sm -let whd_sort_variable (_,sm) t = whd_sort_var sm t -let set_leq_sort_variable (sigma,sm) u1 u2 = - (sigma, set_leq u1 u2 sm) -let define_sort_variable (sigma,sm) u s = - (sigma, set_sort_variable u s sm) -let pr_sort_constraints (_,sm) = pr_sort_cstrs sm +let whd_sort_variable {evars=(_,sm)} t = whd_sort_var sm t +let set_leq_sort_variable ({evars=(sigma,sm)}as d) u1 u2 = + { d with evars = (sigma, set_leq u1 u2 sm) } +let define_sort_variable ({evars=(sigma,sm)}as d) u s = + { d with evars = (sigma, set_sort_variable u s sm) } +let pr_sort_constraints {evars=(_,sm)} = pr_sort_cstrs sm (**********************************************************) (* Accessing metas *) @@ -630,6 +681,7 @@ let meta_with_name evd id = strbrk "\" occurs more than once in clause.") +(* spiwack: we should try and replace this List.fold_left by a Metamap.fold. *) let meta_merge evd1 evd2 = {evd2 with metas = List.fold_left (fun m (n,v) -> Metamap.add n v m) @@ -658,6 +710,19 @@ let subst_defined_metas bl c = | _ -> map_constr substrec c in try Some (substrec c) with Not_found -> None +(*******************************************************************) +type open_constr = evar_map * constr + +(*******************************************************************) +(* The type constructor ['a sigma] adds an evar map to an object of + type ['a] *) +type 'a sigma = { + it : 'a ; + sigma : evar_map} + +let sig_it x = x.it +let sig_sig x = x.sigma + (**********************************************************) (* Failure explanation *) @@ -713,12 +778,12 @@ let pr_evar_info evi = in hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]") -let pr_evar_map sigma = +let pr_evar_defs_t sigma = h 0 (prlist_with_sep pr_fnl (fun (ev,evi) -> h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi)) - (to_list sigma)) + (EvarMap.to_list sigma)) let pr_constraints pbs = h 0 @@ -731,8 +796,8 @@ let pr_constraints pbs = let pr_evar_defs evd = let pp_evm = - if evd.evars = empty then mt() else - str"EVARS:"++brk(0,1)++pr_evar_map evd.evars++fnl() in + if evd.evars = EvarMap.empty then mt() else + str"EVARS:"++brk(0,1)++pr_evar_defs_t evd.evars++fnl() in let cstrs = if evd.conv_pbs = [] then mt() else str"CONSTRAINTS:"++brk(0,1)++pr_constraints evd.conv_pbs++fnl() in diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 6694e63dd..8ea0227fe 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -20,84 +20,6 @@ open Mod_subst open Termops (*i*) -(* The type of mappings for existential variables. - The keys are integers and the associated information is a record - containing the type of the evar ([evar_concl]), the context under which - it was introduced ([evar_hyps]) and its definition ([evar_body]). - [evar_info] is used to add any other kind of information. *) - -type evar = existential_key - -type evar_body = - | Evar_empty - | Evar_defined of constr - -type evar_info = { - evar_concl : constr; - evar_hyps : named_context_val; - evar_body : evar_body; - evar_filter : bool list; - evar_extra : Dyn.t option} - -val eq_evar_info : evar_info -> evar_info -> bool - -val make_evar : named_context_val -> types -> evar_info -val evar_concl : evar_info -> constr -val evar_context : evar_info -> named_context -val evar_filtered_context : evar_info -> named_context -val evar_hyps : evar_info -> named_context_val -val evar_body : evar_info -> evar_body -val evar_filter : evar_info -> bool list -val evar_unfiltered_env : evar_info -> env -val evar_env : evar_info -> env - -type evar_map -val eq_evar_map : evar_map -> evar_map -> bool - -val empty : evar_map - -val add : evar_map -> evar -> evar_info -> evar_map - -val dom : evar_map -> evar list -val find : evar_map -> evar -> evar_info -val remove : evar_map -> evar -> evar_map -val mem : evar_map -> evar -> bool -val to_list : evar_map -> (evar * evar_info) list -val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a - -val merge : evar_map -> evar_map -> evar_map - -val define : evar_map -> evar -> constr -> evar_map - -val is_evar : evar_map -> evar -> bool - -val is_defined : evar_map -> evar -> bool - -val string_of_existential : evar -> string -val existential_of_int : int -> evar - -(*s [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has - no body and [Not_found] if it does not exist in [sigma] *) - -exception NotInstantiatedEvar -val existential_value : evar_map -> existential -> constr -val existential_type : evar_map -> existential -> types -val existential_opt_value : evar_map -> existential -> constr option - -(*********************************************************************) -(* constr with holes *) -type open_constr = evar_map * constr - -(*********************************************************************) -(* The type constructor ['a sigma] adds an evar map to an object of - type ['a] *) -type 'a sigma = { - it : 'a ; - sigma : evar_map} - -val sig_it : 'a sigma -> 'a -val sig_sig : 'a sigma -> evar_map - (*********************************************************************) (* Meta map *) @@ -153,20 +75,92 @@ type clbinding = val map_clb : (constr -> constr) -> clbinding -> clbinding + (*********************************************************************) -(* Unification state *) +(*** Existential variables and unification states ***) + +(* A unification state (of type [evar_defs]) is primarily a finite mapping + from existential variables to records containing the type of the evar + ([evar_concl]), the context under which it was introduced ([evar_hyps]) + and its definition ([evar_body]). [evar_extra] is used to add any other + kind of information. + It also contains conversion constraints, debugging information and + information about meta variables. *) + +(* Information about existential variables. *) +type evar = existential_key + +val string_of_existential : evar -> string +val existential_of_int : int -> evar + +type evar_body = + | Evar_empty + | Evar_defined of constr + +type evar_info = { + evar_concl : constr; + evar_hyps : named_context_val; + evar_body : evar_body; + evar_filter : bool list; + evar_extra : Dyn.t option} + +val eq_evar_info : evar_info -> evar_info -> bool + +val make_evar : named_context_val -> types -> evar_info +val evar_concl : evar_info -> constr +val evar_context : evar_info -> named_context +val evar_filtered_context : evar_info -> named_context +val evar_hyps : evar_info -> named_context_val +val evar_body : evar_info -> evar_body +val evar_filter : evar_info -> bool list +val evar_unfiltered_env : evar_info -> env +val evar_env : evar_info -> env + +(*** Unification state ***) type evar_defs -val subst_evar_map : substitution -> evar_map -> evar_map +(* Unification state and existential variables *) + +(* spiwack: this function seems to be used only for the definition of the progress + tactical. I would recommand not using it in other places. *) +val eq_evar_map : evar_defs -> evar_defs -> bool + +val empty : evar_defs +val is_empty : evar_defs -> bool + +val add : evar_defs -> evar -> evar_info -> evar_defs + +val dom : evar_defs -> evar list +val find : evar_defs -> evar -> evar_info +val remove : evar_defs -> evar -> evar_defs +val mem : evar_defs -> evar -> bool +val to_list : evar_defs -> (evar * evar_info) list +val fold : (evar -> evar_info -> 'a -> 'a) -> evar_defs -> 'a -> 'a + +val merge : evar_defs -> evar_defs -> evar_defs + +val define : evar -> constr -> evar_defs -> evar_defs + +val is_evar : evar_defs -> evar -> bool + +val is_defined : evar_defs -> evar -> bool + +(*s [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has + no body and [Not_found] if it does not exist in [sigma] *) + +exception NotInstantiatedEvar +val existential_value : evar_defs -> existential -> constr +val existential_type : evar_defs -> existential -> types +val existential_opt_value : evar_defs -> existential -> constr option + (* Assume empty universe constraints in [evar_map] and [conv_pbs] *) val subst_evar_defs_light : substitution -> evar_defs -> evar_defs -(* create an [evar_defs] with empty meta map: *) -val create_evar_defs : evar_map -> evar_defs -val create_goal_evar_defs : evar_map -> evar_defs -val empty_evar_defs : evar_defs -val evars_of : evar_defs -> evar_map -val evars_reset_evd : evar_map -> evar_defs -> evar_defs +(* spiwack: this function seems to somewhat break the abstraction. *) +val evars_reset_evd : evar_defs -> evar_defs -> evar_defs + + + (* Should the obligation be defined (opaque or transparent (default)) or defined transparent and expanded in the term? *) @@ -183,17 +177,19 @@ type hole_kind = | TomatchTypeParameter of inductive * int | GoalEvar | ImpossibleCase -val is_defined_evar : evar_defs -> existential -> bool + +(* spiwack: [is_undefined_evar] should be considered a candidate + for moving to evarutils *) val is_undefined_evar : evar_defs -> constr -> bool val undefined_evars : evar_defs -> evar_defs val evar_declare : named_context_val -> evar -> types -> ?src:loc * hole_kind -> ?filter:bool list -> evar_defs -> evar_defs -val evar_define : evar -> constr -> evar_defs -> evar_defs val evar_source : existential_key -> evar_defs -> loc * hole_kind +(* spiwack: this function seesm to somewhat break the abstraction. *) (* [evar_merge evd evars] extends the evars of [evd] with [evars] *) -val evar_merge : evar_defs -> evar_map -> evar_defs +val evar_merge : evar_defs -> evar_defs -> evar_defs (* Unification constraints *) type conv_pb = Reduction.conv_pb @@ -236,11 +232,25 @@ val subst_defined_metas : metabinding list -> constr -> constr option (**********************************************************) (* Sort variables *) -val new_sort_variable : evar_map -> sorts * evar_map -val is_sort_variable : evar_map -> sorts -> bool -val whd_sort_variable : evar_map -> constr -> constr -val set_leq_sort_variable : evar_map -> sorts -> sorts -> evar_map -val define_sort_variable : evar_map -> sorts -> sorts -> evar_map +val new_sort_variable : evar_defs -> sorts * evar_defs +val is_sort_variable : evar_defs -> sorts -> bool +val whd_sort_variable : evar_defs -> constr -> constr +val set_leq_sort_variable : evar_defs -> sorts -> sorts -> evar_defs +val define_sort_variable : evar_defs -> sorts -> sorts -> evar_defs + +(*********************************************************************) +(* constr with holes *) +type open_constr = evar_defs * constr + +(*********************************************************************) +(* The type constructor ['a sigma] adds an evar map to an object of + type ['a] *) +type 'a sigma = { + it : 'a ; + sigma : evar_defs} + +val sig_it : 'a sigma -> 'a +val sig_sig : 'a sigma -> evar_defs (**********************************************************) (* Failure explanation *) @@ -251,7 +261,16 @@ type unsolvability_explanation = SeveralInstancesFound of int (* debug pretty-printer: *) val pr_evar_info : evar_info -> Pp.std_ppcmds -val pr_evar_map : evar_map -> Pp.std_ppcmds val pr_evar_defs : evar_defs -> Pp.std_ppcmds -val pr_sort_constraints : evar_map -> Pp.std_ppcmds +val pr_sort_constraints : evar_defs -> Pp.std_ppcmds val pr_metaset : Metaset.t -> Pp.std_ppcmds + + +(*** /!\Deprecated /!\ ***) +type evar_map = evar_defs +(* create an [evar_defs] with empty meta map: *) +val create_evar_defs : evar_defs -> evar_defs +val create_goal_evar_defs : evar_defs -> evar_defs +val is_defined_evar : evar_defs -> existential -> bool +val subst_evar_map : substitution -> evar_defs -> evar_defs +(*** /Deprecaded ***) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 35c5d376b..0fd2fccb4 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -204,14 +204,14 @@ module Pretyping_F (Coercion : Coercion.S) = struct for i = 0 to lt-1 do if not (e_cumul env evdref (vdefj.(i)).uj_type (lift lt lar.(i))) then - error_ill_typed_rec_body_loc loc env (evars_of !evdref) + error_ill_typed_rec_body_loc loc env ( !evdref) i lna vdefj lar done let check_branches_message loc env evdref c (explft,lft) = for i = 0 to Array.length explft - 1 do if not (e_cumul env evdref lft.(i) explft.(i)) then - let sigma = evars_of !evdref in + let sigma = !evdref in error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i) done @@ -267,7 +267,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct {uj_val=it_mkLambda ccl' sign; uj_type=it_mkProd s' sign} let evar_kind_of_term sigma c = - kind_of_term (whd_evar (Evd.evars_of sigma) c) + kind_of_term (whd_evar ( sigma) c) (*************************************************************************) (* Main pretyping function *) @@ -299,12 +299,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct | REvar (loc, evk, instopt) -> (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) - let hyps = evar_filtered_context (Evd.find (evars_of !evdref) evk) in + let hyps = evar_filtered_context (Evd.find ( !evdref) evk) in let args = match instopt with | None -> instance_from_named_context hyps | Some inst -> failwith "Evar subtitutions not implemented" in let c = mkEvar (evk, args) in - let j = (Retyping.get_judgment_of env (evars_of !evdref) c) in + let j = (Retyping.get_judgment_of env ( !evdref) c) in inh_conv_coerce_to_tycon loc env evdref j tycon | RPatVar (loc,(someta,n)) -> @@ -356,8 +356,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in evar_type_fixpoint loc env evdref names ftys vdefj; - let ftys = Array.map (nf_evar (evars_of !evdref)) ftys in - let fdefs = Array.map (fun x -> nf_evar (evars_of !evdref) (j_val x)) vdefj in + let ftys = Array.map (nf_evar ( !evdref)) ftys in + let fdefs = Array.map (fun x -> nf_evar ( !evdref) (j_val x)) vdefj in let fixj = match fixkind with | RFix (vn,i) -> (* First, let's find the guard indexes. *) @@ -392,7 +392,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct | c::rest -> let argloc = loc_of_rawconstr c in let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in - let resty = whd_betadeltaiota env (evars_of !evdref) resj.uj_type in + let resty = whd_betadeltaiota env ( !evdref) resj.uj_type in match kind_of_term resty with | Prod (na,c1,c2) -> let hj = pretype (mk_tycon c1) env evdref lvar c in @@ -404,19 +404,19 @@ module Pretyping_F (Coercion : Coercion.S) = struct | _ -> let hj = pretype empty_tycon env evdref lvar c in error_cant_apply_not_functional_loc - (join_loc floc argloc) env (evars_of !evdref) + (join_loc floc argloc) env ( !evdref) resj [hj] in let resj = apply_rec env 1 fj args in let resj = match evar_kind_of_term !evdref resj.uj_val with | App (f,args) -> - let f = whd_evar (Evd.evars_of !evdref) f in + let f = whd_evar ( !evdref) f in begin match kind_of_term f with | Ind _ | Const _ when isInd f or has_polymorphic_type (destConst f) -> - let sigma = evars_of !evdref in + let sigma = !evdref in let c = mkApp (f,Array.map (whd_evar sigma) args) in let t = Retyping.get_type_of env sigma c in make_judge c t @@ -454,10 +454,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct | RLetTuple (loc,nal,(na,po),c,d) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env (evars_of !evdref) cj.uj_type + try find_rectype env ( !evdref) cj.uj_type with Not_found -> let cloc = loc_of_rawconstr c in - error_case_not_inductive_loc cloc env (evars_of !evdref) cj + error_case_not_inductive_loc cloc env ( !evdref) cj in let cstrs = get_constructors env indf in if Array.length cstrs <> 1 then @@ -488,7 +488,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct (Array.to_list cs.cs_concl_realargs) @[build_dependent_constructor cs] in let lp = lift cs.cs_nargs p in - let fty = hnf_lam_applist env (evars_of !evdref) lp inst in + let fty = hnf_lam_applist env ( !evdref) lp inst in let fj = pretype (mk_tycon fty) env_f evdref lvar d in let f = it_mkLambda_or_LetIn fj.uj_val fsign in let v = @@ -506,7 +506,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct if noccur_between 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl else - error_cant_find_case_type_loc loc env (evars_of !evdref) + error_cant_find_case_type_loc loc env ( !evdref) cj.uj_val in let ccl = refresh_universes ccl in let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in @@ -520,10 +520,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct | RIf (loc,c,(na,po),b1,b2) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env (evars_of !evdref) cj.uj_type + try find_rectype env ( !evdref) cj.uj_type with Not_found -> let cloc = loc_of_rawconstr c in - error_case_not_inductive_loc cloc env (evars_of !evdref) cj in + error_case_not_inductive_loc cloc env ( !evdref) cj in let cstrs = get_constructors env indf in if Array.length cstrs <> 2 then user_err_loc (loc,"", @@ -542,7 +542,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct | Some p -> let env_p = push_rels psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in - let ccl = nf_evar (evars_of !evdref) pj.utj_val in + let ccl = nf_evar ( !evdref) pj.utj_val in let pred = it_mkLambda_or_LetIn ccl psign in let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in let jtyp = inh_conv_coerce_to_tycon loc env evdref {uj_val = pred; @@ -556,8 +556,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in - let pred = nf_evar (evars_of !evdref) pred in - let p = nf_evar (evars_of !evdref) p in + let pred = nf_evar ( !evdref) pred in + let p = nf_evar ( !evdref) p in let f cs b = let n = rel_context_length cs.cs_args in let pi = lift n pred in (* liftn n 2 pred ? *) @@ -612,7 +612,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct | RDynamic (loc,d) -> if (tag d) = "constr" then let c = constr_out d in - let j = (Retyping.get_judgment_of env (evars_of !evdref) c) in + let j = (Retyping.get_judgment_of env ( !evdref) c) in j (*inh_conv_coerce_to_tycon loc env evdref j tycon*) else @@ -624,7 +624,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct (match valcon with | Some v -> let s = - let sigma = evars_of !evdref in + let sigma = !evdref in let t = Retyping.get_type_of env sigma v in match kind_of_term (whd_betadeltaiota env sigma t) with | Sort s -> s @@ -648,7 +648,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct if e_cumul env evdref v tj.utj_val then tj else error_unexpected_type_loc - (loc_of_rawconstr c) env (evars_of !evdref) tj.utj_val v + (loc_of_rawconstr c) env ( !evdref) tj.utj_val v let pretype_gen_aux evdref env lvar kind c = let c' = match kind with @@ -675,15 +675,15 @@ module Pretyping_F (Coercion : Coercion.S) = struct let evdref = ref (create_evar_defs sigma) in let j = pretype empty_tycon env evdref ([],[]) c in let evd,_ = consider_remaining_unif_problems env !evdref in - let j = j_nf_evar (evars_of evd) j in + let j = j_nf_evar ( evd) j in let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env evd in - let j = j_nf_evar (evars_of evd) j in + let j = j_nf_evar ( evd) j in check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j let understand_judgment_tcc evdref env c = let j = pretype empty_tycon env evdref ([],[]) c in - let sigma = evars_of !evdref in + let sigma = !evdref in let j = j_nf_evar sigma j in j @@ -727,7 +727,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct else pretype_gen_aux evdref env ([],[]) (OfType exptyp) c in !evdref, c - in Evd.evars_of evd, t + in evd, t end module Default : S = Pretyping_F(Coercion.Default) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index cca6b1855..d3bbce9e3 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -376,7 +376,7 @@ exception Partial reduction is solved by the expanded fix term. *) let solve_arity_problem env sigma fxminargs c = let evm = ref sigma in - let set_fix i = evm := Evd.define !evm i (mkVar vfx) in + let set_fix i = evm := Evd.define i (mkVar vfx) !evm in let rec check strict c = let c' = whd_betaiotazeta sigma c in let (h,rcargs) = decompose_app c' in diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index e6b590b03..38e4fb677 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -332,7 +332,7 @@ let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false) let solve_instanciation_problem = ref (fun _ _ _ -> assert false) let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd = - if not (has_typeclasses (Evd.evars_of evd)) then evd + if not (has_typeclasses ( evd)) then evd else !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs split fail diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index ba3eae6fa..fc4362875 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -47,7 +47,7 @@ let unsatisfiable_constraints env evd ev = | None -> raise (TypeClassError (env, UnsatisfiableConstraints (evd, None))) | Some ev -> - let evi = Evd.find (Evd.evars_of evd) ev in + let evi = Evd.find ( evd) ev in let loc, kind = Evd.evar_source ev evd in raise (Stdpp.Exc_located (loc, TypeClassError (env, UnsatisfiableConstraints (evd, Some (evi, kind))))) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index ece3586a1..c22a16048 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -43,30 +43,30 @@ let inductive_type_knowing_parameters env ind jl = let rec execute env evd cstr = match kind_of_term cstr with | Meta n -> - { uj_val = cstr; uj_type = nf_evar (evars_of evd) (meta_type evd n) } + { uj_val = cstr; uj_type = nf_evar ( evd) (meta_type evd n) } | Evar ev -> - let sigma = Evd.evars_of evd in + let sigma = evd in let ty = Evd.existential_type sigma ev in - let jty = execute env evd (nf_evar (evars_of evd) ty) in + let jty = execute env evd (nf_evar ( evd) ty) in let jty = assumption_of_judgment env jty in { uj_val = cstr; uj_type = jty } | Rel n -> - j_nf_evar (evars_of evd) (judge_of_relative env n) + j_nf_evar ( evd) (judge_of_relative env n) | Var id -> - j_nf_evar (evars_of evd) (judge_of_variable env id) + j_nf_evar ( evd) (judge_of_variable env id) | Const c -> - make_judge cstr (nf_evar (evars_of evd) (type_of_constant env c)) + make_judge cstr (nf_evar ( evd) (type_of_constant env c)) | Ind ind -> - make_judge cstr (nf_evar (evars_of evd) (type_of_inductive env ind)) + make_judge cstr (nf_evar ( evd) (type_of_inductive env ind)) | Construct cstruct -> make_judge cstr - (nf_evar (evars_of evd) (type_of_constructor env cstruct)) + (nf_evar ( evd) (type_of_constructor env cstruct)) | Case (ci,p,c,lf) -> let cj = execute env evd c in @@ -101,12 +101,12 @@ let rec execute env evd cstr = (* Sort-polymorphism of inductive types *) make_judge f (inductive_type_knowing_parameters env ind - (jv_nf_evar (evars_of evd) jl)) + (jv_nf_evar ( evd) jl)) | Const cst -> (* Sort-polymorphism of inductive types *) make_judge f (constant_type_knowing_parameters env cst - (jv_nf_evar (evars_of evd) jl)) + (jv_nf_evar ( evd) jl)) | _ -> execute env evd f in @@ -157,7 +157,7 @@ and execute_array env evd = Array.map (execute env evd) and execute_list env evd = List.map (execute env evd) let mcheck env evd c t = - let sigma = Evd.evars_of evd in + let sigma = evd in let j = execute env evd (nf_evar sigma c) in if not (is_conv_leq env sigma j.uj_type t) then error_actual_type env j (nf_evar sigma t) @@ -165,13 +165,13 @@ let mcheck env evd c t = (* Type of a constr *) let mtype_of env evd c = - let j = execute env evd (nf_evar (evars_of evd) c) in + let j = execute env evd (nf_evar ( evd) c) in (* We are outside the kernel: we take fresh universes *) (* to avoid tactics and co to refresh universes themselves *) Termops.refresh_universes j.uj_type let msort_of env evd c = - let j = execute env evd (nf_evar (evars_of evd) c) in + let j = execute env evd (nf_evar ( evd) c) in let a = type_judgment env j in a.utj_type @@ -185,5 +185,5 @@ let check env sigma c = (* The typed type of a judgment. *) let mtype_of_type env evd constr = - let j = execute env evd (nf_evar (evars_of evd) constr) in + let j = execute env evd (nf_evar ( evd) constr) in assumption_of_judgment env j diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 54421f96f..4134f89b2 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -43,14 +43,14 @@ let abstract_scheme env c l lname_typ = lname_typ let abstract_list_all env evd typ c l = - let ctxt,_ = splay_prod_n env (evars_of evd) (List.length l) typ in + let ctxt,_ = splay_prod_n env ( evd) (List.length l) typ in let l_with_all_occs = List.map (function a -> (all_occurrences,a)) l in let p = abstract_scheme env c l_with_all_occs ctxt in try - if is_conv_leq env (evars_of evd) (Typing.mtype_of env evd p) typ then p + if is_conv_leq env ( evd) (Typing.mtype_of env evd p) typ then p else error "abstract_list_all" with UserError _ | Type_errors.TypeError _ -> - error_cannot_find_well_typed_abstraction env (evars_of evd) p l + error_cannot_find_well_typed_abstraction env ( evd) p l (**) @@ -431,14 +431,14 @@ let applyHead env evd n c = if n = 0 then (evd, c) else - match kind_of_term (whd_betadeltaiota env (evars_of evd) cty) with + match kind_of_term (whd_betadeltaiota env ( evd) cty) with | Prod (_,c1,c2) -> let (evd',evar) = Evarutil.new_evar evd env ~src:(dummy_loc,GoalEvar) c1 in apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd' | _ -> error "Apply_Head_Then" in - apprec n c (Typing.type_of env (evars_of evd) c) evd + apprec n c (Typing.type_of env ( evd) c) evd let is_mimick_head f = match kind_of_term f with @@ -468,7 +468,7 @@ let try_to_coerce env evd c cty tycon = let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in let (evd',b) = Evarconv.consider_remaining_unif_problems env evd' in if b then - let evd' = Evd.map_metas_fvalue (nf_evar (evars_of evd')) evd' in + let evd' = Evd.map_metas_fvalue (nf_evar ( evd')) evd' in (evd',j'.uj_val) else error "Cannot solve unification constraints" @@ -481,16 +481,16 @@ let w_coerce_to_type env evd c cty mvty = (* inh_conv_coerce_rigid_to should have reasoned modulo reduction but there are cases where it though it was not rigid (like in fst (nat,nat)) and stops while it could have seen that it is rigid *) - let cty = Tacred.hnf_constr env (evars_of evd) cty in + let cty = Tacred.hnf_constr env ( evd) cty in try_to_coerce env evd c cty tycon let w_coerce env evd mv c = - let cty = get_type_of_with_meta env (evars_of evd) (metas_of evd) c in + let cty = get_type_of_with_meta env ( evd) (metas_of evd) c in let mvty = Typing.meta_type evd mv in w_coerce_to_type env evd c cty mvty let unify_to_type env evd flags c u = - let sigma = evars_of evd in + let sigma = evd in let c = refresh_universes c in let t = get_type_of_with_meta env sigma (metas_of evd) c in let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta evd t)) in @@ -518,7 +518,7 @@ let order_metas metas = let solve_simple_evar_eqn env evd ev rhs = let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (CONV,ev,rhs) in - if not b then error_cannot_unify env (evars_of evd) (mkEvar ev,rhs); + if not b then error_cannot_unify env ( evd) (mkEvar ev,rhs); let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in if not b then error "Cannot solve unification constraints"; evd @@ -534,16 +534,16 @@ let w_merge env with_types flags (metas,evars) evd = match evars with | ((evn,_ as ev),rhs)::evars' -> if is_defined_evar evd ev then - let v = Evd.existential_value (evars_of evd) ev in + let v = Evd.existential_value ( evd) ev in let (metas',evars'') = - unify_0 env (evars_of evd) topconv flags rhs v in + unify_0 env ( evd) topconv flags rhs v in w_merge_rec evd (metas'@metas) (evars''@evars') eqns else begin let rhs' = subst_meta_instances metas rhs in match kind_of_term rhs with | App (f,cl) when is_mimick_head f & occur_meta rhs' -> if occur_evar evn rhs' then - error_occur_check env (evars_of evd) evn rhs'; + error_occur_check env ( evd) evn rhs'; let evd' = mimick_evar evd flags f (Array.length cl) evn in w_merge_rec evd' metas evars eqns | _ -> @@ -568,7 +568,7 @@ let w_merge env with_types flags (metas,evars) evd = if meta_defined evd mv then let {rebus=c'},(status',_) = meta_fvalue evd mv in let (take_left,st,(metas',evars')) = - merge_instances env (evars_of evd) flags status' status c' c + merge_instances env ( evd) flags status' status c' c in let evd' = if take_left then evd @@ -588,16 +588,16 @@ let w_merge env with_types flags (metas,evars) evd = | [] -> evd and mimick_evar evd flags hdc nargs sp = - let ev = Evd.find (evars_of evd) sp in + let ev = Evd.find ( evd) sp in let sp_env = Global.env_of_context ev.evar_hyps in let (evd', c) = applyHead sp_env evd nargs hdc in let (mc,ec) = - unify_0 sp_env (evars_of evd') Cumul flags - (Retyping.get_type_of_with_meta sp_env (evars_of evd') (metas_of evd') c) ev.evar_concl in + unify_0 sp_env ( evd') Cumul flags + (Retyping.get_type_of_with_meta sp_env ( evd') (metas_of evd') c) ev.evar_concl in let evd'' = w_merge_rec evd' mc ec [] in - if (evars_of evd') == (evars_of evd'') - then Evd.evar_define sp c evd'' - else Evd.evar_define sp (Evarutil.nf_evar (evars_of evd'') c) evd'' in + if ( evd') == ( evd'') + then Evd.define sp c evd'' + else Evd.define sp (Evarutil.nf_evar ( evd'') c) evd'' in (* merge constraints *) w_merge_rec evd (order_metas metas) evars [] @@ -617,9 +617,9 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd = types of metavars are unifiable with the types of their instances *) let check_types env evd flags subst m n = - let sigma = evars_of evd in + let sigma = evd in if isEvar (fst (whd_stack sigma m)) or isEvar (fst (whd_stack sigma n)) then - unify_0_with_initial_metas subst true env (evars_of evd) topconv + unify_0_with_initial_metas subst true env ( evd) topconv flags (Retyping.get_type_of_with_meta env sigma (metas_of evd) m) (Retyping.get_type_of_with_meta env sigma (metas_of evd) n) @@ -630,7 +630,7 @@ let w_unify_core_0 env with_types cv_pb flags m n evd = let (mc1,evd') = retract_coercible_metas evd in let subst1 = check_types env evd flags (mc1,[]) m n in let subst2 = - unify_0_with_initial_metas subst1 true env (evars_of evd') cv_pb flags m n + unify_0_with_initial_metas subst1 true env ( evd') cv_pb flags m n in w_merge env with_types flags subst2 evd' @@ -743,8 +743,8 @@ let secondOrderAbstraction env flags allow_K typ (p, oplist) evd = w_merge env false flags ([p,pred,(ConvUpToEta 0,TypeProcessed)],[]) evd' let w_unify2 env flags allow_K cv_pb ty1 ty2 evd = - let c1, oplist1 = whd_stack (evars_of evd) ty1 in - let c2, oplist2 = whd_stack (evars_of evd) ty2 in + let c1, oplist1 = whd_stack ( evd) ty1 in + let c2, oplist2 = whd_stack ( evd) ty2 in match kind_of_term c1, kind_of_term c2 with | Meta p1, _ -> (* Find the predicate *) @@ -782,8 +782,8 @@ let w_unify2 env flags allow_K cv_pb ty1 ty2 evd = Meta(1) had meta-variables in it. *) let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd = let cv_pb = of_conv_pb cv_pb in - let hd1,l1 = whd_stack (evars_of evd) ty1 in - let hd2,l2 = whd_stack (evars_of evd) ty2 in + let hd1,l1 = whd_stack ( evd) ty1 in + let hd2,l2 = whd_stack ( evd) ty2 in match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with (* Pattern case *) | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 62518eaf7..8b7a7d99f 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -80,7 +80,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls = else clenv.evd in tclTHEN - (tclEVARS (evars_of evd')) + (tclEVARS ( evd')) (refine (clenv_cast_meta clenv (clenv_value clenv))) gls @@ -115,7 +115,7 @@ let unifyTerms ?(flags=fail_quick_unif_flags) m n gls = let env = pf_env gls in let evd = create_goal_evar_defs (project gls) in let evd' = w_unify false env CONV ~flags m n evd in - tclIDTAC {it = gls.it; sigma = evars_of evd'} + tclIDTAC {it = gls.it; sigma = evd'} let unify ?(flags=fail_quick_unif_flags) m gls = let n = pf_concl gls in unifyTerms ~flags m n gls diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 17f63933f..e1236bbaa 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -23,20 +23,20 @@ open Refiner (* w_tactic pour instantiate *) let w_refine evk rawc evd = - if Evd.is_defined (evars_of evd) evk then + if Evd.is_defined ( evd) evk then error "Instantiate called on already-defined evar"; - let e_info = Evd.find (evars_of evd) evk in + let e_info = Evd.find ( evd) evk in let env = Evd.evar_env e_info in let sigma,typed_c = try Pretyping.Default.understand_tcc ~resolve_classes:false - (evars_of evd) env ~expected_type:e_info.evar_concl rawc + ( evd) env ~expected_type:e_info.evar_concl rawc with _ -> let loc = Rawterm.loc_of_rawconstr rawc in user_err_loc (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^ string_of_existential evk)) in - evar_define evk typed_c (evars_reset_evd sigma evd) + define evk typed_c (evars_reset_evd sigma evd) (* vernac command Existential *) @@ -56,4 +56,4 @@ let instantiate_pf_com n com pfts = let rawc = Constrintern.intern_constr sigma env com in let evd = create_goal_evar_defs sigma in let evd' = w_refine evk rawc evd in - change_constraints_pftreestate (evars_of evd') pfts + change_constraints_pftreestate ( evd') pfts diff --git a/proofs/logic.ml b/proofs/logic.ml index 7424685bc..5f164b020 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -99,7 +99,7 @@ let check_typability env sigma c = let clear_hyps sigma ids sign cl = let evdref = ref (Evd.create_goal_evar_defs sigma) in let (hyps,concl) = Evarutil.clear_hyps_in_evi evdref sign cl ids in - (hyps,concl,evars_of !evdref) + (hyps,concl, !evdref) (* The ClearBody tactic *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 19ea5c398..f9b7b8677 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -241,9 +241,9 @@ let rec pr_list f = function | a::l1 -> (f a) ++ pr_list f l1 let pr_gls gls = - hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) + hov 0 (pr_evar_defs (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) let pr_glls glls = - hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++ + hov 0 (pr_evar_defs (sig_sig glls) ++ fnl () ++ prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 9d8b6c3b5..672c3d21c 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -390,7 +390,7 @@ let valid goals p res_sigma l = (fun sigma (ev, evi) prf -> let cstr, obls = Refiner.extract_open_proof !res_sigma prf in if not (Evd.is_defined sigma ev) then - Evd.define sigma ev cstr + Evd.define ev cstr sigma else sigma) !res_sigma goals l in raise (Found evm) @@ -402,7 +402,7 @@ let is_dependent ev evm = evm false let resolve_all_evars_once debug (mode, depth) env p evd = - let evm = Evd.evars_of evd in + let evm = evd in let goals, evm' = Evd.fold (fun ev evi (gls, evm') -> @@ -438,7 +438,7 @@ let has_undefined p oevd evd = Evd.fold (fun ev evi has -> has || (evi.evar_body = Evar_empty && p ev evi && (try Typeclasses.is_resolvable (Evd.find oevd ev) with _ -> true))) - (Evd.evars_of evd) false + ( evd) false let rec merge_deps deps = function | [] -> [deps] @@ -459,8 +459,8 @@ let select_evars evs evm = evm Evd.empty let resolve_all_evars debug m env p oevd do_split fail = - let oevm = Evd.evars_of oevd in - let split = if do_split then split_evars (Evd.evars_of (Evd.undefined_evars oevd)) else [Intset.empty] in + let oevm = oevd in + let split = if do_split then split_evars ( (Evd.undefined_evars oevd)) else [Intset.empty] in let p = if do_split then fun comp ev evi -> (Intset.mem ev comp || not (Evd.mem oevm ev)) && p ev evi else fun _ -> p @@ -481,7 +481,7 @@ let resolve_all_evars debug m env p oevd do_split fail = | None -> if fail then (* Unable to satisfy the constraints. *) - let evm = Evd.evars_of evd in + let evm = evd in let evm = if do_split then select_evars comp evm else evm in let _, ev = Evd.fold (fun ev evi (b,acc) -> @@ -615,9 +615,9 @@ let is_applied_setoid_relation t = let head = if isApp c then fst (destApp c) else c in if eq_constr (Lazy.force coq_eq) head then false else (try - let evd, evar = Evarutil.new_evar (Evd.create_evar_defs Evd.empty) (Global.env()) (new_Type ()) in + let evd, evar = Evarutil.new_evar Evd.empty (Global.env()) (new_Type ()) in let inst = mkApp (Lazy.force setoid_relation, [| evar; c |]) in - ignore(Typeclasses.resolve_one_typeclass (Global.env()) (Evd.evars_of evd) inst); + ignore(Typeclasses.resolve_one_typeclass (Global.env()) ( evd) inst); true with _ -> false) | _ -> false @@ -645,19 +645,19 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy. | Some x -> f x in let rec aux env ty l = - let t = Reductionops.whd_betadeltaiota env (Evd.evars_of !isevars) ty in + let t = Reductionops.whd_betadeltaiota env ( !isevars) ty in match kind_of_term t, l with | Prod (na, ty, b), obj :: cstrs -> if dependent (mkRel 1) b then let (b, arg, evars) = aux (Environ.push_rel (na, None, ty) env) b cstrs in - let ty = Reductionops.nf_betaiota (Evd.evars_of !isevars) ty in + let ty = Reductionops.nf_betaiota ( !isevars) ty in let pred = mkLambda (na, ty, b) in let liftarg = mkLambda (na, ty, arg) in let arg' = mkApp (Lazy.force forall_relation, [| ty ; pred ; liftarg |]) in mkProd(na, ty, b), arg', (ty, None) :: evars else let (b', arg, evars) = aux env (subst1 mkProp b) cstrs in - let ty = Reductionops.nf_betaiota(Evd.evars_of !isevars) ty in + let ty = Reductionops.nf_betaiota( !isevars) ty in let relty = mk_relty ty obj in let newarg = mkApp (Lazy.force respectful, [| ty ; b' ; relty ; arg |]) in mkProd(na, ty, b), newarg, (ty, Some relty) :: evars @@ -665,7 +665,7 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy. | _, [] -> (match finalcstr with None -> - let t = Reductionops.nf_betaiota(Evd.evars_of !isevars) ty in + let t = Reductionops.nf_betaiota( !isevars) ty in let rel = mk_relty t None in t, rel, [t, Some rel] | Some codom -> let (t, rel) = Lazy.force codom in @@ -793,7 +793,7 @@ let rewrite2_unif_flags = { } let convertible env evd x y = - Reductionops.is_conv env (Evd.evars_of evd) x y + Reductionops.is_conv env ( evd) x y let allowK = true @@ -803,7 +803,7 @@ let refresh_hypinfo env sigma hypinfo = match c with | Some c -> (* Refresh the clausenv to not get the same meta twice in the goal. *) - hypinfo := decompose_setoid_eqhyp env (Evd.evars_of cl.evd) c l2r; + hypinfo := decompose_setoid_eqhyp env ( cl.evd) c l2r; | _ -> () else () @@ -832,7 +832,7 @@ let unify_eqn env sigma hypinfo t = in let evd' = Typeclasses.resolve_typeclasses ~fail:false env'.env env'.evd in let env' = { env' with evd = evd' } in - let nf c = Evarutil.nf_evar (Evd.evars_of evd') (Clenv.clenv_nf_meta env' c) in + let nf c = Evarutil.nf_evar ( evd') (Clenv.clenv_nf_meta env' c) in let c1 = nf c1 and c2 = nf c2 and car = nf car and rel = nf rel and prf = nf (Clenv.clenv_value env') in @@ -923,7 +923,7 @@ let build_new gl env sigma flags loccs hypinfo concl cstr evars = | Some (env', (prf, hypinfo as x)) when is_occ occ -> begin evars := Evd.evar_merge !evars - (Evd.evars_of (Evd.undefined_evars (Evarutil.nf_evar_defs env'.evd))); + ( (Evd.undefined_evars (Evarutil.nf_evar_defs env'.evd))); match cstr with | None -> Some x, occ | Some _ -> @@ -960,7 +960,7 @@ let build_new gl env sigma flags loccs hypinfo concl cstr evars = let nargs = Array.length args in let res = mkApp (prf, args), - (decomp_prod env (Evd.evars_of !evars) nargs car, + (decomp_prod env ( !evars) nargs car, decomp_pointwise nargs rel, mkApp(c1, args), mkApp(c2, args)) in Some res, occ else rewrite_args occ @@ -1079,7 +1079,7 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g [| mkMeta goal_meta; t |]))) in let evartac = - let evd = Evd.evars_of undef in + let evd = undef in if not (evd = Evd.empty) then Refiner.tclEVARS (Evd.merge sigma evd) else tclIDTAC in tclTHENLIST [evartac; rewtac] gl @@ -1198,7 +1198,7 @@ END (* let depth = match depth with Some i -> i | None -> default_eauto_depth in *) (* match resolve_typeclass_evars d (mode, depth) env evd false with *) (* | Some evd' -> *) -(* let goal = Evd.find (Evd.evars_of evd') 1 in *) +(* let goal = Evd.find ( evd') 1 in *) (* (match goal.evar_body with *) (* | Evar_empty -> tclIDTAC gl *) (* | Evar_defined b -> refine b gl) *) @@ -1431,7 +1431,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 isevars = ref (Evd.create_evar_defs Evd.empty) in + let isevars = ref Evd.empty in let cstrs = let rec aux t = match kind_of_term t with @@ -1459,7 +1459,7 @@ let build_morphism_signature m = let default_morphism sign m = let env = Global.env () in - let isevars = ref (Evd.create_evar_defs Evd.empty) in + let isevars = ref Evd.empty in let t = Typing.type_of env Evd.empty m in let _, sign, evars = build_signature isevars env t (fst sign) (snd sign) (fun (ty, rel) -> rel) @@ -1578,7 +1578,7 @@ let unification_rewrite l2r c1 c2 cl car rel but gl = let mvs = clenv_dependent false cl' in clenv_pose_metas_as_evars cl' mvs in - let nf c = Evarutil.nf_evar (Evd.evars_of cl'.evd) (Clenv.clenv_nf_meta cl' c) in + let nf c = Evarutil.nf_evar ( cl'.evd) (Clenv.clenv_nf_meta cl' c) in let c1 = nf c1 and c2 = nf c2 and car = nf car and rel = nf rel in check_evar_map_of_evars_defs cl'.evd; let prf = nf (Clenv.clenv_value cl') and prfty = nf (Clenv.clenv_type cl') in @@ -1673,13 +1673,13 @@ let typeclass_app_constrexpr t ?(bindings=NoBindings) gl = let t', bl = Tacinterp.intern_constr_with_bindings gs (t,bindings) in let j = Pretyping.Default.understand_judgment_tcc evars env (fst t') in let bindings = Tacinterp.interp_bindings my_ist gl bl in - typeclass_app (Evd.evars_of !evars) gl ~bindings:bindings j.uj_val j.uj_type + typeclass_app ( !evars) gl ~bindings:bindings j.uj_val j.uj_type let typeclass_app_raw t gl = let env = pf_env gl in let evars = ref (create_evar_defs (project gl)) in let j = Pretyping.Default.understand_judgment_tcc evars env t in - typeclass_app (Evd.evars_of !evars) gl j.uj_val j.uj_type + typeclass_app ( !evars) gl j.uj_val j.uj_type let pr_gen prc _prlc _prtac c = prc c diff --git a/tactics/equality.ml b/tactics/equality.ml index dd9f648ca..0d8187984 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -566,7 +566,7 @@ exception NotDiscriminable let eq_baseid = id_of_string "e" let apply_on_clause (f,t) clause = - let sigma = Evd.evars_of clause.evd in + let sigma = clause.evd in let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in let argmv = (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with @@ -588,7 +588,7 @@ let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort = [onLastHyp gen_absurdity; refine pf] let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls = - let sigma = Evd.evars_of eq_clause.evd in + let sigma = eq_clause.evd in let env = pf_env gls in match find_positions env sigma t1 t2 with | Inr _ -> @@ -608,7 +608,7 @@ let onEquality with_evars tac (c,lbindc) gls = with PatternMatchingFailure -> errorlabstrm "" (str"No primitive equality found.") in tclTHEN - (Refiner.tclEVARS (Evd.evars_of eq_clause'.evd)) + (Refiner.tclEVARS ( eq_clause'.evd)) (tac eq eq_clause') gls let onNegatedEquality with_evars tac gls = @@ -739,21 +739,21 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = else error "Cannot solve an unification problem." else - let (a,p_i_minus_1) = match whd_beta_stack (evars_of !evdref) p_i with + let (a,p_i_minus_1) = match whd_beta_stack ( !evdref) p_i with | (_sigS,[a;p]) -> (a,p) | _ -> anomaly "sig_clausal_form: should be a sigma type" in let ev = Evarutil.e_new_evar evdref env a in let rty = beta_applist(p_i_minus_1,[ev]) in let tuple_tail = sigrec_clausal_form (siglen-1) rty in match - Evd.existential_opt_value (Evd.evars_of !evdref) + Evd.existential_opt_value ( !evdref) (destEvar ev) with | Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) | None -> anomaly "Not enough components to build the dependent tuple" in let scf = sigrec_clausal_form siglen ty in - Evarutil.nf_evar (Evd.evars_of !evdref) scf + Evarutil.nf_evar ( !evdref) scf (* The problem is to build a destructor (a generalization of the predecessor) which, when applied to a term made of constructors @@ -891,7 +891,7 @@ exception Not_dep_pair let injEq ipats (eq,(t,t1,t2)) eq_clause = - let sigma = Evd.evars_of eq_clause.evd in + let sigma = eq_clause.evd in let env = eq_clause.env in match find_positions env sigma t1 t2 with | Inl _ -> @@ -953,7 +953,7 @@ let injHyp id gls = injClause [] false (Some (ElimOnIdent (dummy_loc,id))) gls let decompEqThen ntac (lbeq,(t,t1,t2) as u) clause gls = let sort = pf_apply get_type_of gls (pf_concl gls) in - let sigma = Evd.evars_of clause.evd in + let sigma = clause.evd in let env = pf_env gls in match find_positions env sigma t1 t2 with | Inl (cpath, (_,dirn), _) -> diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 5e87d432b..d03b26192 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -54,7 +54,7 @@ let instantiate n rawc ido gl = let ev,_ = destEvar (List.nth evl (n-1)) in let evd' = w_refine ev rawc (create_goal_evar_defs sigma) in tclTHEN - (tclEVARS (evars_of evd')) + (tclEVARS ( evd')) tclNORMEVAR gl @@ -74,6 +74,6 @@ let instantiate_tac = function let let_evar name typ gls = let evd = Evd.create_goal_evar_defs gls.sigma in let evd',evar = Evarutil.new_evar evd (pf_env gls) typ in - Refiner.tclTHEN (Refiner.tclEVARS (evars_of evd')) + Refiner.tclTHEN (Refiner.tclEVARS ( evd')) (Tactics.letin_tac None name evar None nowhere) gls diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 9ca68c9a1..0129c06c8 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1427,14 +1427,14 @@ let solvable_by_tactic env evi (ev,args) src = let solve_remaining_evars env initial_sigma evd c = let evdref = ref (Typeclasses.resolve_typeclasses ~fail:true env evd) in let rec proc_rec c = - match kind_of_term (Reductionops.whd_evar (evars_of !evdref) c) with + match kind_of_term (Reductionops.whd_evar ( !evdref) c) with | Evar (ev,args as k) when not (Evd.mem initial_sigma ev) -> let (loc,src) = evar_source ev !evdref in - let sigma = evars_of !evdref in + let sigma = !evdref in let evi = Evd.find sigma ev in (try let c = solvable_by_tactic env evi k src in - evdref := Evd.evar_define ev c !evdref; + evdref := Evd.define ev c !evdref; c with Exit -> Pretype_errors.error_unsolvable_implicit loc env sigma evi src None) @@ -1466,11 +1466,11 @@ let interp_econstr kind ist sigma env cc = (* Interprets an open constr *) let interp_open_constr ccl ist sigma env cc = let evd,c = interp_gen (OfType ccl) ist sigma env cc in - (evars_of evd,c) + ( evd,c) let interp_open_type ccl ist sigma env cc = let evd,c = interp_gen IsType ist sigma env cc in - (evars_of evd,c) + ( evd,c) let interp_constr = interp_econstr (OfType None) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0bcdcc8fd..b45861fd3 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -528,7 +528,7 @@ let resolve_classes gl = if evd = Evd.empty then tclIDTAC gl else let evd' = Typeclasses.resolve_typeclasses env (Evd.create_evar_defs evd) in - (tclTHEN (tclEVARS (Evd.evars_of evd')) tclNORMEVAR) gl + (tclTHEN (tclEVARS ( evd')) tclNORMEVAR) gl (**************************) (* Cut tactics *) @@ -577,7 +577,7 @@ let clenv_refine_in with_evars ?(with_classes=true) id clenv gl = error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in tclTHEN - (tclEVARS (evars_of clenv.evd)) + (tclEVARS ( clenv.evd)) (cut_replacing id new_hyp_typ (fun x gl -> refine_no_check new_hyp_prf gl)) gl @@ -747,7 +747,7 @@ let check_evars sigma evm gl = in if rest <> Evd.empty then errorlabstrm "apply" (str"Uninstantiated existential variables: " ++ - fnl () ++ pr_evar_map rest) + fnl () ++ pr_evar_defs rest) let general_apply with_delta with_destruct with_evars (c,lbind) gl0 = let flags = @@ -985,7 +985,7 @@ let specialize mopt (c,lbind) g = let clause = make_clenv_binding g (c,pf_type_of g c) lbind in let clause = clenv_unify_meta_types clause in let (thd,tstack) = - whd_stack (evars_of clause.evd) (clenv_value clause) in + whd_stack ( clause.evd) (clenv_value clause) in let nargs = List.length tstack in let tstack = match mopt with | Some m -> @@ -1001,7 +1001,7 @@ let specialize mopt (c,lbind) g = errorlabstrm "" (str "Cannot infer an instance for " ++ pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++ str "."); - Some (evars_of clause.evd), term + Some ( clause.evd), term in tclTHEN (match evars with Some e -> tclEVARS e | _ -> tclIDTAC) @@ -3164,5 +3164,5 @@ let unify ?(state=full_transparent_state) x y gl = in let evd = w_unify false (pf_env gl) Reduction.CONV ~flags x y (Evd.create_evar_defs (project gl)) - in tclEVARS (Evd.evars_of evd) gl + in tclEVARS ( evd) gl with _ -> tclFAIL 0 (str"Not unifiable") gl diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 8a9646a17..520f9b631 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -53,15 +53,15 @@ let subst_evar_in_evm evar def evm = * T1, c : T2 and T1 /= T2. Defines recursively all evars instantiated * by this definition. *) -let rec safe_evar_define evm ev c = +let rec safe_define evm ev c = if not (closedn (-1) c) then raise Termops.CannotFilter else -(* msgnl(str"safe_evar_define "++pr_evar_map evm++spc()++str" |- ?"++Util.pr_int ev++str" := "++pr_constr c);*) +(* msgnl(str"safe_define "++pr_evar_defs evm++spc()++str" |- ?"++Util.pr_int ev++str" := "++pr_constr c);*) let evi = (Evd.find evm ev) in let define_subst evm sigma = Util.Intmap.fold ( fun ev (e,c) evm -> match kind_of_term c with Evar (i,_) when i=ev -> evm | _ -> - safe_evar_define evm ev (lift (-List.length e) c) + safe_define evm ev (lift (-List.length e) c) ) sigma evm in match evi.evar_body with | Evd.Evar_defined def -> @@ -70,7 +70,7 @@ let rec safe_evar_define evm ev c = let t = Libtypes.reduce (Typing.type_of (Global.env()) evm c) in let u = Libtypes.reduce (evar_concl evi) in let evm = subst_evar_in_evm ev c evm in - define_subst (Evd.define evm ev c) (Termops.filtering [] Reduction.CUMUL t u) + define_subst (Evd.define ev c evm) (Termops.filtering [] Reduction.CUMUL t u) let add_gen_ctx (cl,gen,evm) ctx : signature * constr list = let rec really_new_evar () = @@ -111,9 +111,9 @@ let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) = let def = applistc (Libnames.constr_of_global gr) argl in (* msgnl(str"essayons ?"++Util.pr_int ev++spc()++str":="++spc() ++pr_constr def++spc()++str":"++spc()++pr_constr (Global.type_of_global gr)*) - (*++spc()++str"dans"++spc()++pr_evar_map evm++spc());*) + (*++spc()++str"dans"++spc()++pr_evar_defs evm++spc());*) try - let evm = safe_evar_define evm ev def in + let evm = safe_define evm ev def in k (cl,gen,evm); if sort_is_prop && SubstSet.mem s !substs then raise Exit; substs := SubstSet.add s !substs @@ -147,10 +147,10 @@ let complete_with_evars_permut (cl,gen,evm:signature) evl c (k:signature -> unit let tyl = List.map (fun (_,_,t) -> t) ctx in let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) tyl in let def = applistc c argl in -(* msgnl(str"trouvĂ© def ?"++Util.pr_int ev++str" := "++pr_constr def++str " dans "++pr_evar_map evm);*) +(* msgnl(str"trouvĂ© def ?"++Util.pr_int ev++str" := "++pr_constr def++str " dans "++pr_evar_defs evm);*) try if not (Evd.is_defined evm ev) then - let evm = safe_evar_define evm ev def in + let evm = safe_define evm ev def in aux evm; k (cl,gen,evm) with Termops.CannotFilter -> () ) evl in @@ -220,7 +220,7 @@ let complete_signature_with_def gr deftyp (k:instance_decl_function -> signature ( fun ctx typ -> List.iter (fun ((cl,ev,evm),_,_) -> -(* msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Util.pr_int ev++str " dans "++pr_evar_map evm);*) +(* msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Util.pr_int ev++str " dans "++pr_evar_defs evm);*) smap := Gmapl.add (cl,evm) (ctx,ev) !smap) (Recordops.methods_matching typ) ) [] deftyp; @@ -263,7 +263,7 @@ let declare_instance (k:global_reference -> rel_context -> constr list -> unit) then Evd.remove evm ev,gen else evm,(ev::gen)) gen (evm,[]) in -(* msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Util.pr_int gen++str"] : "++spc()++pr_evar_map evm);*) +(* msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Util.pr_int gen++str"] : "++spc()++pr_evar_defs evm);*) let ngen = List.length gen in let (_,ctx,evm) = List.fold_left ( fun (i,ctx,evm) ev -> diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 081d18292..b6c664020 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -72,7 +72,7 @@ type binder_list = (identifier located * bool * constr_expr) list (* Calls to interpretation functions. *) let interp_type_evars evdref env ?(impls=([],[])) typ = - let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in + let typ' = intern_gen true ~impls ( !evdref) env typ in let imps = Implicit_quantifiers.implicits_of_rawterm typ' in imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ' @@ -133,7 +133,7 @@ let declare_instance_constant k pri global imps ?hook id term termtype = let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri = let env = Global.env() in - let isevars = ref (Evd.create_evar_defs Evd.empty) in + let isevars = ref Evd.empty in let tclass = match bk with | Implicit -> @@ -169,7 +169,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) let env' = push_rel_context ctx' env in isevars := Evarutil.nf_evar_defs !isevars; isevars := resolve_typeclasses env !isevars; - let sigma = Evd.evars_of !isevars in + let sigma = !isevars in let subst = List.map (Evarutil.nf_evar sigma) subst in if Lib.is_modtype () then begin @@ -234,9 +234,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) let term = Termops.it_mkLambda_or_LetIn app ctx' in isevars := Evarutil.nf_evar_defs !isevars; let term = Evarutil.nf_isevar !isevars term in - let evm = Evd.evars_of (undefined_evars !isevars) in + let evm = (undefined_evars !isevars) in Evarutil.check_evars env Evd.empty !isevars termtype; - if evm = Evd.empty then + if Evd.is_empty evm then declare_instance_constant k pri global imps ?hook id term termtype else begin isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !isevars; @@ -246,7 +246,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) (fun _ -> function ConstRef cst -> instance_hook k pri global imps ?hook cst | _ -> assert false); if props <> [] then - Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *) + Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS ( !isevars)) *) (!refine_ref (evm, term)); (match tac with Some tac -> Pfedit.by tac | None -> ())) (); Flags.if_verbose (msg $$ Printer.pr_open_subgoals) (); @@ -266,9 +266,9 @@ let named_of_rel_context l = let context ?(hook=fun _ -> ()) l = let env = Global.env() in - let evars = ref (Evd.create_evar_defs Evd.empty) in + let evars = ref Evd.empty in let (env', fullctx), impls = interp_context_evars evars env l in - let fullctx = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) fullctx in + let fullctx = Evarutil.nf_rel_context_evar ( !evars) fullctx in let ce t = Evarutil.check_evars env Evd.empty !evars t in List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx; let ctx = try named_of_rel_context fullctx with _ -> diff --git a/toplevel/command.ml b/toplevel/command.ml index 1ab819a5e..50c78d0ed 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -115,7 +115,7 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) = | Some comtyp -> let ty = generalize_constr_expr comtyp bl in let b = abstract_constr_expr com bl in - let evdref = ref (Evd.create_evar_defs Evd.empty) in + let evdref = ref Evd.empty in let ty, impls = interp_type_evars_impls ~evdref env ty in let b, imps = interp_casted_constr_evars_impls ~evdref env b ty in let body, typ = nf_isevar !evdref b, nf_isevar !evdref ty in @@ -509,7 +509,7 @@ let check_all_names_different indl = if l <> [] then raise (InductiveError (SameNamesOverlap l)) let mk_mltype_data evdref env assums arity indname = - let is_ml_type = is_sort env (evars_of !evdref) arity in + let is_ml_type = is_sort env ( !evdref) arity in (is_ml_type,indname,assums) let prepare_param = function @@ -530,7 +530,7 @@ let interp_cstrs evdref env impls mldata arity ind = let interp_mutual paramsl indl notations finite = check_all_names_different indl; let env0 = Global.env() in - let evdref = ref (Evd.create_evar_defs Evd.empty) in + let evdref = ref Evd.empty in let (env_params, ctx_params), userimpls = interp_context_evars ~fail_anonymous:false evdref env0 paramsl in @@ -562,7 +562,7 @@ let interp_mutual paramsl indl notations finite = (* Instantiate evars and check all are resolved *) let evd,_ = consider_remaining_unif_problems env_params !evdref in let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in - let sigma = evars_of evd in + let sigma = evd in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in let arities = List.map (nf_evar sigma) arities in @@ -846,12 +846,12 @@ let interp_recursive fixkind l boxed = let fixnames = List.map (fun fix -> fix.fix_name) fixl in (* Interp arities allowing for unresolved types *) - let evdref = ref (Evd.create_evar_defs Evd.empty) in + let evdref = ref Evd.empty in let fixctxs, fiximps = List.split (List.map (interp_fix_context evdref env) fixl) in let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in let fixtypes = List.map2 build_fix_type fixctxs fixccls in - let fixtypes = List.map (nf_evar (evars_of !evdref)) fixtypes in + let fixtypes = List.map (nf_evar ( !evdref)) fixtypes in let env_rec = push_named_types env fixnames fixtypes in (* Get interpretation metadatas *) @@ -867,8 +867,8 @@ let interp_recursive fixkind l boxed = (* Instantiate evars and check all are resolved *) let evd,_ = consider_remaining_unif_problems env_rec !evdref in - let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in - let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in + let fixdefs = List.map (nf_evar ( evd)) fixdefs in + let fixtypes = List.map (nf_evar ( evd)) fixtypes in let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in List.iter (check_evars env_rec Evd.empty evd) fixdefs; List.iter (check_evars env Evd.empty evd) fixtypes; diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 42fc6d0fc..e8ca54c9c 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -522,10 +522,10 @@ let pr_constraints printenv env evm = prlist_with_sep (fun () -> fnl ()) (fun (ev, evi) -> str(string_of_existential ev)++ str " == " ++ pr_constr evi.evar_concl) l else - pr_evar_map evm + pr_evar_defs evm let explain_unsatisfiable_constraints env evd constr = - let evm = Evd.evars_of evd in + let evm = evd in match constr with | None -> str"Unable to satisfy the following constraints:" ++ fnl() ++ diff --git a/toplevel/record.ml b/toplevel/record.ml index 10d4e5dc6..fe478f080 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -32,7 +32,7 @@ open Topconstr (********** definition d'un record (structure) **************) let interp_evars evdref env ?(impls=([],[])) k typ = - let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in + let typ' = intern_gen true ~impls ( !evdref) env typ in let imps = Implicit_quantifiers.implicits_of_rawterm typ' in imps, Pretyping.Default.understand_tcc_evars evdref env k typ' @@ -64,7 +64,7 @@ let binders_of_decls = List.map binder_of_decl let typecheck_params_and_fields id t ps nots fs = let env0 = Global.env () in - let evars = ref (Evd.create_evar_defs Evd.empty) in + let evars = ref Evd.empty in let (env1,newps), imps = interp_context_evars ~fail_anonymous:false evars env0 ps in let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (new_Type ()) t) newps in let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in @@ -73,7 +73,7 @@ let typecheck_params_and_fields id t ps nots fs = in let evars,_ = Evarconv.consider_remaining_unif_problems env_ar !evars in let evars = Typeclasses.resolve_typeclasses env_ar evars in - let sigma = Evd.evars_of evars in + let sigma = evars in let newps = Evarutil.nf_rel_context_evar sigma newps in let newfs = Evarutil.nf_rel_context_evar sigma newfs in let ce t = Evarutil.check_evars env0 Evd.empty evars t in |