diff options
| author | Pierre Roux | 2019-11-13 11:34:15 +0100 |
|---|---|---|
| committer | Pierre Roux | 2019-11-13 13:28:18 +0100 |
| commit | 64239322013a30cf25b2a1ca4a8f66bff8a7d818 (patch) | |
| tree | 1c5beec05de5a10296ea729c3859a5de42d79d94 | |
| parent | c45f079c52524da687dfcc9e5f5511d6e86bc537 (diff) | |
Register proof_irrelevance
| -rw-r--r-- | theories/Logic/ProofIrrelevance.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v index e4fbd1c273..4cbbef2757 100644 --- a/theories/Logic/ProofIrrelevance.v +++ b/theories/Logic/ProofIrrelevance.v @@ -14,6 +14,8 @@ Require Import ProofIrrelevanceFacts. Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2. +Register proof_irrelevance as core.proof_irrelevance. + Module PI. Definition proof_irrelevance := proof_irrelevance. End PI. Module ProofIrrelevanceTheory := ProofIrrelevanceTheory(PI). |