From 8cb5e072d095981aa0664ca9b6f3db8983e18437 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Wed, 17 Aug 2005 12:56:38 +0000
Subject: new congruence

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

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index ea51ca76f6..aa9aac6489 100644
--- a/Makefile
+++ b/Makefile
@@ -291,7 +291,8 @@ FOCMO=\
   contrib/first-order/instances.cmo contrib/first-order/ground.cmo \
   contrib/first-order/g_ground.cmo
 
-CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo  
+CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo \
+  contrib/cc/g_congruence.cmo 
 
 SUBTACCMO=\
 	contrib/subtac/natural.cmo \
@@ -306,7 +307,7 @@ SUBTACCMO=\
 RTAUTOCMO=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \
 	contrib/rtauto/g_rtauto.cmo
 
-ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/cctac.ml4 \
+ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/g_congruence.ml4 \
   contrib/funind/tacinv.ml4 contrib/first-order/g_ground.ml4 \
   contrib/subtac/sparser.ml4 contrib/subtac/g_eterm.ml4 \
   contrib/rtauto/g_rtauto.ml4
@@ -1004,8 +1005,7 @@ FUNINDVO=
 
 JPROVERVO= 
 
-CCVO=\
- contrib/cc/CCSolve.vo
+CCVO=
 
 SUBTACVO=
 
-- 
cgit v1.2.3