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
---
 tactics/tacinterp.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ee4e61179b..f24297cf05 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -45,6 +45,7 @@ open Printer
 open Inductiveops
 open Syntax_def
 open Pretyping
+open Pretyping.Default
 
 let error_syntactic_metavariables_not_allowed loc =
   user_err_loc 
-- 
cgit v1.2.3