diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-06-30 15:18:21 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-07-01 17:26:02 +0200 |
| commit | 3e1e8e5792b43be83da2cca8102418aa9b73b9b3 (patch) | |
| tree | f46ebf80ac216adddf32bff2386114e0bf4d5ef0 /tactics | |
| parent | e57aab0559297cff3875931258674cfe2cfbbba3 (diff) | |
Make semantics of whd_zeta consistent with other whd_* functions.
whd_zeta now takes an evar_map and looks in evar instances. This changes
the behavior of whd_zeta e.g. on let x := ?t in x
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 1950356b3..24028b09d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -400,7 +400,8 @@ let type_of_clause cls gl = match cls with let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl = Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> - let isatomic = isProd (whd_zeta hdcncl) in + let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let isatomic = isProd (whd_zeta evd hdcncl) in let dep_fun = if isatomic then dependent else dependent_no_evar in let type_of_cls = type_of_clause cls gl in let dep = dep_proof_ok && dep_fun c type_of_cls in |