diff options
| author |  jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-28 12:17:22 +0000 |
|---|---|---|
| committer | jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-28 12:17:22 +0000 |
| commit | db3a9e3e16d6d7c6bc66b90a0f2eaf72ea28f81e (patch) | |
| tree | 61f5ab09559d4337d1254f795d8d02e2fdd76981 /Makefile.common | |
| parent | 3478ffda0a0a83951db341eb68fc6b71877c1392 (diff) | |
menage dans funind + deplaceemnt de recdef dans funind
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10865 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/Makefile.common b/Makefile.common index e45d70b99..315ed912a 100644 --- a/Makefile.common +++ b/Makefile.common @@ -274,14 +274,12 @@ JPROVERCMO:=\ FUNINDCMO:=\ contrib/funind/indfun_common.cmo contrib/funind/rawtermops.cmo \ + contrib/funind/recdef.cmo \ contrib/funind/rawterm_to_relation.cmo \ contrib/funind/functional_principles_proofs.cmo \ contrib/funind/functional_principles_types.cmo \ contrib/funind/invfun.cmo contrib/funind/indfun.cmo \ - contrib/funind/merge.cmo contrib/funind/indfun_main.cmo - -RECDEFCMO:=\ - contrib/recdef/recdef.cmo + contrib/funind/merge.cmo contrib/funind/g_indfun.cmo FOCMO:=\ contrib/firstorder/formula.cmo contrib/firstorder/unify.cmo \ @@ -307,7 +305,7 @@ RTAUTOCMO:=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \ CONTRIB:=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(NEWRINGCMO) $(DPCMO) $(FIELDCMO) \ $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \ $(CCCMO) $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \ - $(RECDEFCMO) $(FUNINDCMO) + $(FUNINDCMO) CMA:=$(CLIBS) $(CAMLP4OBJS) CMXA:=$(CMA:.cma=.cmxa) @@ -797,7 +795,7 @@ FOURIERVO:=\ FUNINDVO:= -RECDEFVO:=contrib/recdef/Recdef.vo +RECDEFVO:=contrib/funind/Recdef.vo JPROVERVO:= |