diff options
| author | Emilio Jesus Gallego Arias | 2019-11-21 18:56:49 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-11-21 18:56:49 +0100 |
| commit | af98bb689a05ccf420da53ee7befacb7c2202942 (patch) | |
| tree | 972e28fd5779f101fab9001556010e3986de2c79 | |
| parent | 1b33b57f56f4d53d20318fe9be97dec274086f5b (diff) | |
| parent | 64239322013a30cf25b2a1ca4a8f66bff8a7d818 (diff) | |
Merge PR #11109: Register proof_irrelevance
Ack-by: SkySkimmer
Reviewed-by: ejgallego
| -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). |