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.itarget4
1 files changed, 3 insertions, 1 deletions
diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget
index 323597395..71d01c1fb 100644
--- a/theories/Logic/vo.itarget
+++ b/theories/Logic/vo.itarget
@@ -20,6 +20,7 @@ WeakFan.vo
WKL.vo
FunctionalExtensionality.vo
ExtensionalityFacts.vo
+ExtensionalFunctionRepresentative.vo
Hurkens.vo
IndefiniteDescription.vo
JMeq.vo
@@ -27,4 +28,5 @@ ProofIrrelevanceFacts.vo
ProofIrrelevance.vo
RelationalChoice.vo
SetIsType.vo
-FinFun.vo \ No newline at end of file
+SetoidChoice.vo
+FinFun.vo