diff options
| -rw-r--r-- | pretyping/coercion.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4782.v | 15 |
2 files changed, 16 insertions, 1 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index d00445958..71c55ae05 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -510,7 +510,7 @@ let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t = error_actual_type_loc loc env best_failed_evd cj t e else inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t - with NoCoercionNoUnifier (best_failed_evd,e) -> + with NoCoercionNoUnifier (_evd,_error) -> error_actual_type_loc loc env best_failed_evd cj t e in let val' = match val' with Some v -> v | None -> assert(false) in diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v index ed4443786..dbd71035d 100644 --- a/test-suite/bugs/closed/4782.v +++ b/test-suite/bugs/closed/4782.v @@ -7,3 +7,18 @@ Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p. Goal p. Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil. +(* A simplification of an example from coquelicot, which was failing + at some time after a fix #4782 was committed. *) + +Record T := { dom : Type }. +Definition pairT A B := {| dom := (dom A * dom B)%type |}. +Class C (A:Type). +Parameter B:T. +Instance c (A:T) : C (dom A). +Instance cn : C (dom B). +Parameter F : forall A:T, C (dom A) -> forall x:dom A, x=x -> A = A. +Set Typeclasses Debug. +Goal forall (A:T) (x:dom A), pairT A A = pairT A A. +intros. +apply (F _ _) with (x,x). + |