diff options
| -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). |