diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 48 | ||||
| -rw-r--r-- | tactics/equality.ml | 16 | ||||
| -rw-r--r-- | tactics/evar_tactics.ml | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 10 | ||||
| -rw-r--r-- | tactics/tactics.ml | 12 |
5 files changed, 45 insertions, 45 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 9d8b6c3b57..672c3d21cc 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 dd9f648caa..0d81879843 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 5e87d432ba..d03b26192c 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 9ca68c9a18..0129c06c87 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 0bcdcc8fd4..b45861fd33 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 |