diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-17 17:34:05 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-17 17:34:05 +0200 |
| commit | 258cbd1d2619cc5916dd570b95050e37c06fba77 (patch) | |
| tree | 7f4a5cb362b4fe4fe062f6dd542943504ad99e46 /pretyping/evarconv.ml | |
| parent | 35d92d68c0b2123a3994a90ef7e2b8cbb946f041 (diff) | |
Reinstate eta for records in evarconv, fixing two HoTT coq bugs.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 22 |
1 files changed, 14 insertions, 8 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d93574b47..2761dcbe3 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -616,6 +616,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Construct _, Construct _ -> rigids env evd sk1 term1 sk2 term2 + | Construct u, _ -> + eta_constructor ts env evd sk1 u sk2 term2 + + | _, Construct u -> + eta_constructor ts env evd sk2 u sk1 term1 + | Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *) if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then ise_and evd [ @@ -643,9 +649,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (Stack.zip (term1,sk1')) (Stack.zip (term2,sk2')) end - | (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _), _ -> + | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _), _ -> UnifFailure (evd,NotSameHead) - | _, (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _) -> + | _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _) -> UnifFailure (evd,NotSameHead) | (App _ | Cast _ | Case _ | Proj _), _ -> assert false @@ -687,23 +693,23 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1), (fst (decompose_app_vect (substl ks h'))))] else UnifFailure(evd,(*dummy*)NotSameHead) -(*and eta_constructor ts env evd ((ind, i), u) l1 csts1 (c, csts2) = +and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with | Some (exp,projs) when Array.length projs > 0 -> let pars = mib.Declarations.mind_nparams in (try - let l1' = Stack.tail pars l1 in + let l1' = Stack.tail pars sk1 in if Environ.is_projection projs.(0) env then - let sk2 = - let term = Stack.zip c in + let l2' = + let term = Stack.zip (term2,sk2) in List.map (fun p -> mkProj (p, term)) (Array.to_list projs) in exact_ise_stack2 env evd (evar_conv_x ts) l1' - (Stack.append_app_list sk2 Stack.empty) + (Stack.append_app_list l2' Stack.empty) else raise (Failure "") with Failure _ -> UnifFailure(evd,NotSameHead)) - | _ -> UnifFailure (evd,NotSameHead)*) + | _ -> UnifFailure (evd,NotSameHead) (* Profiling *) let evar_conv_x = |