Mercurial > cpdt > repo

comparison src/Universes.v @ 574:1dc1d41620b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.15.2
author Adam Chlipala <adam@chlipala.net>
date Sun, 31 Jul 2022 14:48:22 -0400
parents 0ce9829efa3b
children
comparison
equal deleted inserted replaced
573:c3d77f2bb92c 574:1dc1d41620b6
6 * The license text is available at: 6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import List. 11 Require Import List Lia.
12 Hint Extern 2 False => lia.
13 Hint Extern 2 (@eq nat _ _) => lia.
12 14
13 Require Import DepList Cpdt.CpdtTactics. 15 Require Import DepList Cpdt.CpdtTactics.
14 16
15 Require Extraction. 17 Require Extraction.
16 18