From a869d74f414ba786c66b8eb7450ff6343ff12ebd Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 16 Dec 2008 12:57:26 +0000
Subject: Move FunctionalExtensionality to Logic/ (someone please check that
 the doc is ok). Rework the .v files in Program accordingly, adding some
 documentation and proper headers. Integrate the development of an elimination
 principle for measured functions in Program/Wf by Eelis van der Weegen.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11686 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.common | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index cefdfd4e19..4ca7e2e45b 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -543,7 +543,7 @@ LOGICVO:=$(addprefix theories/Logic/, \
  EqdepFacts.vo            ProofIrrelevanceFacts.vo ClassicalEpsilon.vo 	\
  ClassicalUniqueChoice.vo DecidableType.vo         DecidableTypeEx.vo 	\
  Epsilon.vo               ConstructiveEpsilon.vo   Description.vo 	\
- IndefiniteDescription.vo SetIsType.vo )
+ IndefiniteDescription.vo SetIsType.vo             FunctionalExtensionality.vo )
 
 ARITHVO:=$(addprefix theories/Arith/, \
  Arith.vo	Gt.vo          	Between.vo	Le.vo         	\
@@ -740,8 +740,7 @@ CLASSESVO:=$(addprefix theories/Classes/, \
 
 PROGRAMVO:=$(addprefix theories/Program/, \
  Tactics.vo 	Equality.vo 	Subset.vo	Utils.vo 	\
- Wf.vo 		Basics.vo	FunctionalExtensionality.vo 	\
- Combinators.vo	Syntax.vo 	Program.vo )
+ Wf.vo 		Basics.vo	Combinators.vo	Syntax.vo 	Program.vo )
 
 THEORIESVO:=\
   $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \
-- 
cgit v1.2.3