aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic/vo.itarget
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Logic/vo.itarget')
-rw-r--r--theories/Logic/vo.itarget5
1 files changed, 4 insertions, 1 deletions
diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget
index 323597395..ef2709b47 100644
--- a/theories/Logic/vo.itarget
+++ b/theories/Logic/vo.itarget
@@ -20,11 +20,14 @@ WeakFan.vo
WKL.vo
FunctionalExtensionality.vo
ExtensionalityFacts.vo
+ExtensionalFunctionRepresentative.vo
Hurkens.vo
IndefiniteDescription.vo
JMeq.vo
ProofIrrelevanceFacts.vo
ProofIrrelevance.vo
+PropExtensionality.vo
RelationalChoice.vo
SetIsType.vo
-FinFun.vo \ No newline at end of file
+SetoidChoice.vo
+FinFun.vo