diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-11-08 12:39:34 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-08 12:39:34 +0100 |
commit | 7e42041f5c4711a9fece32ce601ef99ca8ab272f (patch) | |
tree | f2330be6cbe2a8d0be1a7de17875c7ed62770e1f /pretyping | |
parent | 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff) | |
parent | dd56ef10395a2ced84612aa799690b034306806e (diff) |
Merge PR #922: New beta-iota compatibility refinements
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/pretyping.ml | 7 | ||||
-rw-r--r-- | pretyping/unification.ml | 4 |
2 files changed, 11 insertions, 0 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a69caecab..b2b583ba7 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -888,6 +888,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | [], [] -> [] | _ -> assert false in aux 1 1 (List.rev nal) cs.cs_args, true in + let fsign = if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + then Context.Rel.map (whd_betaiota !evdref) fsign + else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in let obj ind p v f = if not record then let nal = List.map (fun na -> ltac_interp_name lvar na) nal in @@ -997,6 +1000,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let pi = lift n pred in (* liftn n 2 pred ? *) let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in + let cs_args = + if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + then Context.Rel.map (whd_betaiota !evdref) cs_args + else cs_args (* beta-iota-normalization regression in 8.5 and 8.6 *) in let csgn = List.map (set_name Anonymous) cs_args in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index e8f7e2bba..86ebc1f01 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; |