diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-26 22:29:23 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-21 12:38:09 +0200 |
commit | 9490c6099e1da94fcf315aba48125993cd180327 (patch) | |
tree | 4a73cd1032b6ae47ca094b67fa20de29d38adf5d /pretyping/unification.ml | |
parent | 325890a83a2b073d9654b5615c585cd65a376fbd (diff) |
Fixing a new regresssion with 8.4 wrt to βι-normalization of created hyps.
Formerly, mk_refgoals in logic.ml was applying full βι on new Meta-based goals.
We simulate part of this βι-normalization in pose_all_metas_as_evars.
I suspect that we don't βι-normalize goals more than in 8.4 by doing
that, since all Metas would have eventually gone to mk_refgoals, but
difficult to know for sure as there were probably metas turned to
evars (and hence a priori not βι-normalized) even when logic.ml was
used more pervasively.
However, βι-normalizing is a priori a better heuristic than no
βι-normalizing, independently of what it was in 8.4 and before (even
if, ideally, I would personally lean towards preferring a
"chirurgical" substitution with reduction only at the place of
substitution).
Diffstat (limited to 'pretyping/unification.ml')
-rw-r--r-- | pretyping/unification.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f090921e5..61160147a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -194,6 +194,10 @@ let pose_all_metas_as_evars env evd t = let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in let ty = EConstr.of_constr ty in let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in + let ty = + if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + then nf_betaiota evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *) + else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in let src = Evd.evar_source_of_meta mv !evdref in let ev = Evarutil.e_new_evar env evdref ~src ty in evdref := meta_assign mv (EConstr.Unsafe.to_constr ev,(Conv,TypeNotProcessed)) !evdref; |