aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-10-27 10:29:17 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-10-27 10:32:11 +0100
commitb56ec63bf021a8dd95ce2eddc365115ce818a43e (patch)
tree2e59c203dc99925ae762baa0335d2d8ac506f96a /theories/Logic
parent6bb322f5ac542d12cf482b8bf02d2ee46c950a66 (diff)
Make sure that Logic/ExtensionalityFacts gets compiled.
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 6f7eba904..323597395 100644
--- a/theories/Logic/vo.itarget
+++ b/theories/Logic/vo.itarget
@@ -19,6 +19,7 @@ Eqdep.vo
WeakFan.vo
WKL.vo
FunctionalExtensionality.vo
+ExtensionalityFacts.vo
Hurkens.vo
IndefiniteDescription.vo
JMeq.vo