diff options
| -rw-r--r-- | pretyping/evarconv.ml | 26 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3319.v (renamed from test-suite/bugs/opened/3319.v) | 17 |
2 files changed, 20 insertions, 23 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index ca0644c47e..53b4526c2c 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -396,21 +396,21 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f1; (consume_stack on_left apprF apprM); f3] in let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) = let switch f a b = if on_left then f a b else f b a in - match Stack.list_of_app_stack skF with + let f1 evd = + match Stack.list_of_app_stack skF with | None -> consume_stack on_left apprF apprR evd | Some lF -> - let f1 evd = - miller_pfenning on_left - (fun () -> (* Postpone the use of an heuristic *) - switch (fun x y -> - Success (add_conv_pb (pbty,env,Stack.zip x,Stack.zip y) evd)) apprF apprR) - ev lF apprR evd - and f2 evd = - if isLambda termR then - eta env evd false skR termR skF termF - else UnifFailure (evd,NotSameHead) - in ise_try evd [f1;f2] in - + miller_pfenning on_left + (fun () -> (* Postpone the use of an heuristic *) + switch (fun x y -> + Success (add_conv_pb (pbty,env,Stack.zip x,Stack.zip y) evd)) apprF apprR) + ev lF apprR evd + in + let f2 evd = + if isLambda termR then + eta env evd false skR termR skF termF + else UnifFailure (evd,NotSameHead) + in ise_try evd [f1;f2] in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in (* Evar must be undefined since we have flushed evars *) let () = if !debug_unification then diff --git a/test-suite/bugs/opened/3319.v b/test-suite/bugs/closed/3319.v index 7851a08ea4..bb5853ddd3 100644 --- a/test-suite/bugs/opened/3319.v +++ b/test-suite/bugs/closed/3319.v @@ -3,6 +3,7 @@ Set Implicit Arguments. Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. + Record PreCategory := { obj :> Type; morphism : obj -> obj -> Type }. Record NotionOfStructure (X : PreCategory) := { structure :> X -> Type; @@ -14,15 +15,11 @@ Section precategory. Variable P : NotionOfStructure X. Local Notation object := { x : X & P x }. Record morphism' (xa yb : object) := {}. - Fail Lemma issig_morphism xa yb + + Lemma issig_morphism xa yb : { f : morphism X (projT1 xa) (projT1 yb) & is_structure_homomorphism _ _ _ f (projT2 xa) (projT2 yb) } - = morphism' xa yb. (* Toplevel input, characters 169-171: -Error: -In environment -X : PreCategory -P : NotionOfStructure X -xa : {x : _ & ?26 x} -yb : {x : _ & ?26 x} -The term "xa" has type "{x : _ & ?26 x}" while it is expected to have type - "{x : X & P x}". *) + = morphism' xa yb. + Proof. + admit. + Defined.
\ No newline at end of file |