Better type_inversion

Now we don't loop on [Unit = Unit] hypotheses, clearing them instead.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/Reflection/TypeInversion.v b/src/Reflection/TypeInversion.v
index 15986d1a5..30a1ef472 100644
--- a/src/Reflection/TypeInversion.v
+++ b/src/Reflection/TypeInversion.v
@@ -69,9 +69,10 @@ Section language.
   Section encode_decode.
     Definition flat_type_code (t1 t2 : flat_type base_type_code) : Prop
       := match t1, t2 with
-         | Unit, _ => Unit = t2
+         | Unit, Unit => True
          | Tbase t1, Tbase t2 => t1 = t2
          | Prod A B, Prod A' B' => A = A' /\ B = B'
+         | Unit, _
          | Tbase _, _
          | Prod _ _, _
            => False
@@ -96,7 +97,6 @@ Section language.
       destruct x, y; simpl in *; intro H;
         try first [ apply f_equal; assumption
                   | exfalso; assumption
-                  | exfalso; abstract congruence
                   | reflexivity
                   | apply f_equal2; destruct H; assumption ].
     Defined.