From af354d63a814b0855eefda81852029d72b3544db Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 29 May 2006 19:59:11 +0000
Subject: The "clean integration of subtac" patch. Adds a new kind of casts
 (CastCoerce) for coercing an object to its base type (e.g. inductive). The
 new cast_type type subsumes usual casts ConvCasts. Much of the patch is just
 adding ConvCasts where needed. The Pretyping module has been adapted to this
 change, although it doesn't change anything yet, but this construct could
 have a use with current coercions also. Pretyping is also cleaned from the
 "Use type constraints under lambdas" patch which is not yet ready for wide
 use. It has been transferred to a copy of the Pretyping Functor in
 subtac_pretyping_F.ml. Subtac is now working as well as I demonstrated at
 TYPES.

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

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 70e20ac72e..fe8d729084 100644
--- a/Makefile
+++ b/Makefile
@@ -301,6 +301,7 @@ SUBTACCMO=\
 	contrib/subtac/context.cmo \
 	contrib/subtac/subtac_errors.cmo \
 	contrib/subtac/subtac_coercion.cmo \
+	contrib/subtac/subtac_pretyping_F.cmo \
 	contrib/subtac/subtac_pretyping.cmo \
 	contrib/subtac/subtac_interp_fixpoint.cmo \
 	contrib/subtac/subtac_command.cmo \
-- 
cgit v1.2.3