aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--pretyping/evarconv.ml42
-rw-r--r--test-suite/bugs/closed/3480.v47
2 files changed, 77 insertions, 12 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 53b4526c2..53c560f86 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -466,7 +466,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
| MaybeFlexible (v1,sk1), Flexible ev2 ->
flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) (v1,sk1)
- | MaybeFlexible (v1,sk1), MaybeFlexible (v2,sk2) -> begin
+ | MaybeFlexible (v1,sk1'), MaybeFlexible (v2,sk2') -> begin
match kind_of_term term1, kind_of_term term2 with
| LetIn (na,b1,t1,c'1), LetIn (_,b2,_,c'2) ->
let f1 i =
@@ -476,10 +476,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let b = nf_evar i b1 in
let t = nf_evar i t1 in
evar_conv_x ts (push_rel (na,Some b,t) env) i pbty c'1 c'2);
- (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
+ (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1' sk2')]
and f2 i =
- let out1 = whd_betaiota_deltazeta_for_iota_state ts env i csts1 (v1,sk1)
- and out2 = whd_betaiota_deltazeta_for_iota_state ts env i csts2 (v2,sk2)
+ let out1 = whd_betaiota_deltazeta_for_iota_state ts env i csts1 (v1,sk1')
+ and out2 = whd_betaiota_deltazeta_for_iota_state ts env i csts2 (v2,sk2')
in evar_eqappr_x ts env i pbty out1 out2
in
ise_try evd [f1; f2]
@@ -488,13 +488,31 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let f1 i =
ise_and i
[(fun i -> evar_conv_x ts env i CONV c c');
- (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
+ (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1' sk2')]
and f2 i =
- let out1 = whd_betaiota_deltazeta_for_iota_state ts env i csts1 (v1,sk1)
- and out2 = whd_betaiota_deltazeta_for_iota_state ts env i csts2 (v2,sk2)
+ let out1 = whd_betaiota_deltazeta_for_iota_state ts env i csts1 (v1,sk1')
+ and out2 = whd_betaiota_deltazeta_for_iota_state ts env i csts2 (v2,sk2')
in evar_eqappr_x ts env i pbty out1 out2
in
ise_try evd [f1; f2]
+
+ | Proj (p, t), Const (p',_) when eq_constant p p' ->
+ let pb = Environ.lookup_projection p env in
+ (match Stack.strip_n_app pb.Declarations.proj_npars sk2' with
+ | Some (pars, t', rest) ->
+ ise_and evd
+ [(fun i -> evar_conv_x ts env i CONV t t');
+ (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 rest)]
+ | None -> UnifFailure (evd, NotSameHead))
+
+ | Const (p',_), Proj (p, t) when eq_constant p p' ->
+ let pb = Environ.lookup_projection p env in
+ (match Stack.strip_n_app pb.Declarations.proj_npars sk1' with
+ | Some (pars, t', rest) ->
+ ise_and evd
+ [(fun i -> evar_conv_x ts env i CONV t t');
+ (fun i -> exact_ise_stack2 env i (evar_conv_x ts) rest sk2)]
+ | None -> UnifFailure (evd, NotSameHead))
| _, _ ->
let f1 i =
@@ -509,7 +527,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
try Success (Evd.add_universe_constraints i univs)
with UniversesDiffer -> UnifFailure (i,NotSameHead)
| Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
- (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
+ (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1' sk2')]
else UnifFailure (i,NotSameHead)
and f2 i =
(try conv_record ts env i
@@ -535,7 +553,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
| Proj (p, c) -> true
| Case _ | App _| Cast _ -> assert false in
let rhs_is_stuck_and_unnamed () =
- let applicative_stack = fst (Stack.strip_app sk2) in
+ let applicative_stack = fst (Stack.strip_app sk2') in
is_unnamed
(fst (whd_betaiota_deltazeta_for_iota_state
ts env i Cst_stack.empty (v2, applicative_stack))) in
@@ -543,15 +561,15 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in
if (isLambda term1 || rhs_is_already_stuck)
- && (not (Stack.not_purely_applicative sk1)) then
+ && (not (Stack.not_purely_applicative sk1')) then
evar_eqappr_x ~rhs_is_already_stuck ts env i pbty
(whd_betaiota_deltazeta_for_iota_state
- ts env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
+ ts env i (Cst_stack.add_cst term1 csts1) (v1,sk1'))
(appr2,csts2)
else
evar_eqappr_x ts env i pbty (appr1,csts1)
(whd_betaiota_deltazeta_for_iota_state
- ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
+ ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2'))
in
ise_try evd [f1; f2; f3]
end
diff --git a/test-suite/bugs/closed/3480.v b/test-suite/bugs/closed/3480.v
new file mode 100644
index 000000000..99ac2efab
--- /dev/null
+++ b/test-suite/bugs/closed/3480.v
@@ -0,0 +1,47 @@
+Set Primitive Projections.
+Axiom admit : forall {T}, T.
+Notation "( x ; y )" := (existT _ x y) : fibration_scope.
+Open Scope fibration_scope.
+Notation "x .1" := (projT1 x) (at level 3) : fibration_scope.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Set Implicit Arguments.
+Delimit Scope category_scope with category.
+Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
+Local Open Scope category_scope.
+Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := { morphism_inverse : morphism C d s }.
+Class Isomorphic {C : PreCategory} s d := { morphism_isomorphic :> @morphism C s d ; isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }.
+Coercion morphism_isomorphic : Isomorphic >-> morphism.
+Local Infix "<~=~>" := Isomorphic (at level 70, no associativity) : category_scope.
+Definition idtoiso (C : PreCategory) (x y : C) (H : x = y) : Isomorphic x y := admit.
+Record NotionOfStructure (X : PreCategory) := { structure :> X -> Type }.
+Record Smorphism (X : PreCategory) (P : NotionOfStructure X) (xa yb : { x : X & P x }) := { f : morphism X xa.1 yb.1 }.
+Definition precategory_of_structures X (P : NotionOfStructure X) : PreCategory.
+Proof.
+ refine (@Build_PreCategory _ (@Smorphism _ P)).
+Defined.
+Section sip.
+ Variable X : PreCategory.
+ Variable P : NotionOfStructure X.
+
+ Let StrX := @precategory_of_structures X P.
+
+ Definition sip_isotoid (xa yb : StrX) (f : xa <~=~> yb) : xa = yb.
+ admit.
+ Defined.
+
+ Lemma structure_identity_principle_helper (xa yb : StrX)
+ (x : xa <~=~> yb) : Smorphism P xa yb.
+ Proof.
+ refine ((idtoiso (precategory_of_structures P) (sip_isotoid x) : @morphism _ _ _) : morphism _ _ _).
+(* Toplevel input, characters 24-95:
+Error:
+In environment
+X : PreCategory
+P : NotionOfStructure X
+StrX := precategory_of_structures P : PreCategory
+xa : object StrX
+yb : object StrX
+x : xa <~=~> yb
+The term "morphism_isomorphic:@morphism (precategory_of_structures P) xa yb"
+has type "@morphism (precategory_of_structures P) xa yb"
+while it is expected to have type "morphism ?40 ?41 ?42". *) \ No newline at end of file