diff src/Universes.v @ 574:1dc1d41620b6

Builds with Coq 8.15.2
author Adam Chlipala <adam@chlipala.net>
date Sun, 31 Jul 2022 14:48:22 -0400
parents 0ce9829efa3b
children
line wrap: on
line diff
--- a/src/Universes.v	Sun Feb 02 10:51:18 2020 -0500
+++ b/src/Universes.v	Sun Jul 31 14:48:22 2022 -0400
@@ -8,7 +8,9 @@
  *)
 
 (* begin hide *)
-Require Import List.
+Require Import List Lia.
+Hint Extern 2 False => lia.
+Hint Extern 2 (@eq nat _ _) => lia.
 
 Require Import DepList Cpdt.CpdtTactics.