Make congruence reuse discriminate instead of rolling its own.

This changes the produced terms a bit, eg

Axiom T : Type.
Lemma foo : true = false -> T.
Proof. congruence. Qed.

used to produce

fun H : true = false =>
let Heq := H : true = false in
@eq_rect Type True (fun X : Type => X) I T
  (@f_equal bool Type (fun t : bool => if t then True else T) true false Heq)

now produces

fun H : true = false =>
let Heq : true = false := H in
let H0 : False := @eq_ind bool true (fun e : bool => if e then True else False) I false Heq in
False_rect T H0

i.e. instead of proving [True = T] by [f_equal] then transporting [I]
across this identity, it now proves [False] by [eq_ind] then uses exfalso.

0 files changed, 0 insertions, 0 deletions