diff options
| -rw-r--r-- | pretyping/evarconv.ml | 22 | ||||
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_104.v (renamed from test-suite/bugs/opened/HoTT_coq_104.v) | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_124.v (renamed from test-suite/bugs/opened/HoTT_coq_124.v) | 4 |
3 files changed, 17 insertions, 11 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 = diff --git a/test-suite/bugs/opened/HoTT_coq_104.v b/test-suite/bugs/closed/HoTT_coq_104.v index ff2da3948..5bb7fa8c1 100644 --- a/test-suite/bugs/opened/HoTT_coq_104.v +++ b/test-suite/bugs/closed/HoTT_coq_104.v @@ -10,4 +10,4 @@ Local Set Primitive Projections. Record prod (A B : Type) : Type := pair { fst : A; snd : B }. -Fail Check fun x : prod Set Set => eq_refl : x = pair (fst x) (snd x). +Check fun x : prod Set Set => eq_refl : x = pair (fst x) (snd x). diff --git a/test-suite/bugs/opened/HoTT_coq_124.v b/test-suite/bugs/closed/HoTT_coq_124.v index 2854c3ee4..e6e90ada8 100644 --- a/test-suite/bugs/opened/HoTT_coq_124.v +++ b/test-suite/bugs/closed/HoTT_coq_124.v @@ -9,7 +9,7 @@ Monomorphic Record prodm (A B : Type) : Type := pairm { fstm : A; sndm : B }. Check eqm_refl _ : eqm (fun x : prodm Set Set => pairm (fstm x) (sndm x)) (fun x => x). (* success *) Check eqp_refl _ : eqp (fun x : prodm Set Set => pairm (fstm x) (sndm x)) (fun x => x). (* success *) -Fail Check eqm_refl _ : eqm (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error: +Check eqm_refl _ : eqm (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error: The term "eqm_refl (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})" has type @@ -18,7 +18,7 @@ has type while it is expected to have type "eqm (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |}) (fun x : prodp Set Set => x)". *) -Fail Check eqp_refl _ : eqp (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error: +Check eqp_refl _ : eqp (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error: The term "eqp_refl (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})" has type |