diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eauto.ml | 10 | ||||
| -rw-r--r-- | tactics/wcclausenv.ml | 4 |
2 files changed, 3 insertions, 11 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index f86262b5cf..38bb223420 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -103,17 +103,9 @@ let instantiate_tac = function (fun gl -> instantiate n c gl) | _ -> invalid_arg "Instantiate called with bad arguments" -let whd_evar env sigma c = match kind_of_term c with - | IsEvar (n, cl) when Evd.in_dom sigma n & Evd.is_defined sigma n -> - Instantiate.existential_value sigma (n,cl) - | _ -> c - let normEvars gl = let sigma = project gl in - let env = pf_env gl in - let nf_evar = strong whd_evar - and simplify = nf_betaiota in - convert_concl (nf_evar env sigma (simplify env sigma (pf_concl gl))) gl + convert_concl (nf_betaiota (Evarutil.nf_evar sigma (pf_concl gl))) gl let vernac_prolog = let uncom = function diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml index 3215cf017c..63504956c8 100644 --- a/tactics/wcclausenv.ml +++ b/tactics/wcclausenv.ml @@ -91,8 +91,8 @@ let clenv_constrain_with_bindings bl clause = in let env = Global.env () in let sigma = Evd.empty in - let k_typ = nf_betaiota env sigma (clenv_instance_type clause k) in - let c_typ = nf_betaiota env sigma (w_type_of clause.hook c) in + let k_typ = nf_betaiota (clenv_instance_type clause k) in + let c_typ = nf_betaiota (w_type_of clause.hook c) in matchrec (clenv_assign k c (clenv_unify k_typ c_typ clause)) t in matchrec clause bl |