From 030b0fb6b0b81095df515c1ddb9662c575d503bf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Mon, 22 Aug 2016 14:02:19 +0200
Subject: [PATCH] Now really get rid of the eq_rect_eq axiom.
The previous commit is not really necesarry anymore, but my proof
for UIP of types with decidable equality is a bit more general, so
I won't revert it.
---
theories/numbers.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/numbers.v b/theories/numbers.v
index a85776e..30dfb57 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -3,7 +3,7 @@
(** This file collects some trivial facts on the Coq types [nat] and [N] for
natural numbers, and the type [Z] for integers. It also declares some useful
notations. *)
-From Coq Require Export Eqdep PArith NArith ZArith NPeano.
+From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
From Coq Require Import QArith Qcanon.
From stdpp Require Export base decidable option.
Open Scope nat_scope.
--
GitLab