aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-03-28 16:29:15 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-03-28 16:32:25 +0200
commit45985baf2262504a9fb8f24e7960caa9f11d29f3 (patch)
treebcc91ed8ff183a77c6eee35a739652da20ce2a07 /theories/Logic
parent7535e268f7706d1dee263fdbafadf920349103db (diff)
Fixing missing PropFacts.v in Logic/vo.itarget.
This is while waiting for a possible different solution, if ever such a different solution is adopted, since the coq.inria.fr/library has currently a broken link and someone rightly complained about it.
Diffstat (limited to 'theories/Logic')
-rw-r--r--theories/Logic/vo.itarget1
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget
index 8b0aa6691..5eba0b623 100644
--- a/theories/Logic/vo.itarget
+++ b/theories/Logic/vo.itarget
@@ -27,6 +27,7 @@ IndefiniteDescription.vo
JMeq.vo
ProofIrrelevanceFacts.vo
ProofIrrelevance.vo
+PropFacts.vo
PropExtensionality.vo
RelationalChoice.vo
SetIsType.vo