From 10961655cb9c09da20cfe2ecc68def3d3b7d1bb5 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 22 Mar 2006 15:36:58 +0000
Subject: Made pretyping a functor over a coercion implementation.
 Pretyping.Default uses the original Coercion implementation. Updated
 contributions that called pretyping to use the default impl. Also update
 subtac using the functor, do some renamings and add interfaces for all files.

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

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index aca30acbaa..ebafe9f33a 100644
--- a/Makefile
+++ b/Makefile
@@ -293,16 +293,17 @@ CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo \
   contrib/cc/g_congruence.cmo 
 
 SUBTACCMO=\
-	contrib/subtac/scoq.cmo \
+	contrib/subtac/subtac_utils.cmo \
 	contrib/subtac/eterm.cmo \
+	contrib/subtac/g_eterm.cmo \
 	contrib/subtac/context.cmo \
 	contrib/subtac/subtac_errors.cmo \
 	contrib/subtac/subtac_coercion.cmo \
-	contrib/subtac/interp.cmo \
-	contrib/subtac/interp_fixpoint.cmo \
+	contrib/subtac/subtac_pretyping.cmo \
+	contrib/subtac/subtac_interp_fixpoint.cmo \
 	contrib/subtac/subtac_command.cmo \
 	contrib/subtac/subtac.cmo \
-	contrib/subtac/sparser.cmo
+	contrib/subtac/g_subtac.cmo
 
 
 RTAUTOCMO=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \
@@ -310,7 +311,7 @@ RTAUTOCMO=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \
 
 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/subtac/g_subtac.ml4 contrib/subtac/g_eterm.ml4 \
 	contrib/rtauto/g_rtauto.ml4 contrib/recdef/recdef.ml4 \
 	contrib/funind/indfun_main.ml4 
 
-- 
cgit v1.2.3