diff options
author | 2015-01-03 15:41:14 +0100 | |
---|---|---|
committer | 2015-01-03 16:03:18 +0100 | |
commit | 353b523c0c808d0650cd77821363b0c865aedecf (patch) | |
tree | 7ec71e045ed1d80b60d63b55b36e766344ab83c9 | |
parent | 3bd9cb26be01d0791fdf2dc56d3aacaa1379e50c (diff) |
Fixing #3895 (thanks to PMP for diagnosis).
-rw-r--r-- | pretyping/evarsolve.ml | 4 | ||||
-rw-r--r-- | test-suite/bugs/closed/3895.v | 22 |
2 files changed, 24 insertions, 2 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 1a1cd92ed..f8518beaa 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1128,8 +1128,8 @@ let solve_evar_evar_aux f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) with CannotProject (evd,ev2) -> add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd -let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = - let (evd,ev1,ev2),pbty = +let solve_evar_evar ?(force=false) f g env evd pbty ev1 ev2 = + let (evd,(evk1,args1 as ev1),(evk2,args2 as ev2)),pbty = (* If an evar occurs in the instance of the other evar and the use of an heuristic is forced, we restrict *) if force then ensure_evar_independent g env evd ev1 ev2, None diff --git a/test-suite/bugs/closed/3895.v b/test-suite/bugs/closed/3895.v new file mode 100644 index 000000000..8659ca2cb --- /dev/null +++ b/test-suite/bugs/closed/3895.v @@ -0,0 +1,22 @@ +Notation pr1 := (@projT1 _ _). +Notation compose := (fun g' f' x => g' (f' x)). +Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : +function_scope. +Open Scope function_scope. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p +with eq_refl => eq_refl end. +Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) := forall x:A, +f x = g x. +Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : +type_scope. +Theorem Univalence_implies_FunextNondep (A B : Type) +: forall f g : A -> B, f == g -> f = g. +Proof. + intros f g p. + pose (d := fun x : A => existT (fun xy => fst xy = snd xy) (f x, f x) +(eq_refl (f x))). + pose (e := fun x : A => existT (fun xy => fst xy = snd xy) (f x, g x) (p x)). + change f with ((snd o pr1) o d). + change g with ((snd o pr1) o e). + apply (ap (fun g => snd o pr1 o g)). +(* Used to raise a not Found due to a "typo" in solve_evar_evar *) |