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
---
 contrib/recdef/recdef.ml4 | 1 +
 1 file changed, 1 insertion(+)

(limited to 'contrib/recdef')

diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index f973548457..36ebaff11f 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -34,6 +34,7 @@ open Pfedit
 open Topconstr
 open Rawterm
 open Pretyping
+open Pretyping.Default
 open Safe_typing
 open Constrintern
 open Hiddentac
-- 
cgit v1.2.3