diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 4 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 10 | ||||
| -rw-r--r-- | proofs/logic.ml | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 4 |
4 files changed, 10 insertions, 10 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 62518eaf74..8b7a7d99f6 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 17f63933f9..e1236bbaa8 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 7424685bc9..5f164b020f 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 19ea5c398d..f9b7b8677d 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)) |