diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-29 00:10:43 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-29 00:19:04 +0200 |
| commit | 6e22ae3f21ae32f298b6e3463448f59a5c7d1f76 (patch) | |
| tree | 1408ca239b7153725c7a77195c6ab3f39ec27d7d /pretyping/evarutil.ml | |
| parent | 199bb343f7e4367d843ab5ae76ba9a4de89eddbc (diff) | |
In evarconv and unification, expand folded primitive projections to
their eta-expanded forms which can then unfold back to the unfolded
primitive projection form. This removes all special code that
was necessary to handle primitive projections before, while keeping
compatibility.
Also fix cbn which was not refolding primitive projections correctly
in all cases.
Update some test-suite files accordingly.
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index f02d7623d..7b1fee543 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -705,7 +705,8 @@ let define_pure_evar_as_product evd evk = let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in - let s = destSort evi.evar_concl in + let concl = whd_evar evd evi.evar_concl in + let s = destSort concl in let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in let evd2,rng = let newenv = push_named (id, None, dom) evenv in @@ -713,7 +714,7 @@ let define_pure_evar_as_product evd evk = let filter = Filter.extend 1 (evar_filter evi) in if is_prop_sort s then (* Impredicative product, conclusion must fall in [Prop]. *) - new_evar newenv evd1 evi.evar_concl ~src ~filter + new_evar newenv evd1 concl ~src ~filter else let evd3, (rng, srng) = new_type_evar newenv evd1 univ_flexible_alg ~src ~filter in |