From b01b06d3a843c97adc6c0a0621b8d681c10fa6fe Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Tue, 16 Nov 2004 15:49:08 +0000
Subject: Names.substitution (and related functions) and Term.subst_mps moved
 to the new module kernel/mod_subst.ml.

MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now
possible to define substitutions that also delta-expand constants
(by associating the delta-expanded form to the constant name).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/extract_env.ml | 1 +
 contrib/extraction/modutil.ml     | 1 +
 contrib/extraction/modutil.mli    | 1 +
 contrib/field/field.ml4           | 1 +
 contrib/ring/ring.ml              | 1 +
 5 files changed, 5 insertions(+)

(limited to 'contrib')

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 78fb578e99..8c75f2df5c 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -19,6 +19,7 @@ open Table
 open Extraction
 open Modutil
 open Common
+open Mod_subst
 
 (*s Obtaining Coq environment. *)
 
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index 1a40a83307..673c8e929d 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -16,6 +16,7 @@ open Util
 open Miniml
 open Table
 open Mlutil
+open Mod_subst
 
 (*S Functions upon modules missing in [Modops]. *) 
 
diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli
index ec628b329e..07425c30af 100644
--- a/contrib/extraction/modutil.mli
+++ b/contrib/extraction/modutil.mli
@@ -13,6 +13,7 @@ open Declarations
 open Environ
 open Libnames
 open Miniml
+open Mod_subst
 
 (*s Functions upon modules missing in [Modops]. *) 
 
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 02393f1b75..94044cf20b 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -21,6 +21,7 @@ open Util
 open Vernacinterp
 open Vernacexpr
 open Tacexpr
+open Mod_subst
 
 (* Interpretation of constr's *)
 let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index bf45397983..1eb4783d14 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -34,6 +34,7 @@ open Pattern
 open Hiddentac
 open Nametab
 open Quote
+open Mod_subst
 
 let mt_evd = Evd.empty
 let constr_of c = Constrintern.interp_constr mt_evd (Global.env()) c
-- 
cgit v1.2.3