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

12 files changed, 13 insertions, 1 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 7fb1bb2ccc..aef35cd7cf 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -21,6 +21,7 @@ open Term
 open Termops
 open Rawterm
 open Decl_kinds
+open Mod_subst
 
 (* usage qque peu general: utilise aussi dans record *)
 
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 0ce44b5073..c1590f6a89 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -15,6 +15,7 @@ open Term
 open Evd
 open Environ
 open Nametab
+open Mod_subst
 (*i*)
 
 (*s This is the type of class kinds *)
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 981692ebdb..4b8ed1ed11 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -26,6 +26,7 @@ open Tacred
 open Pretype_errors
 open Evarutil
 open Unification
+open Mod_subst
 
 (* *)
 let w_coerce env c ctyp target evd =
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 0c19a60f98..3208bd5931 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -16,6 +16,7 @@ open Sign
 open Environ
 open Evd
 open Evarutil
+open Mod_subst
 (*i*)
 
 (***************************************************************)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 26b646bdd8..6a0ea00602 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -24,6 +24,7 @@ open Termops
 open Libnames
 open Nametab
 open Evd
+open Mod_subst
 
 (****************************************************************************)
 (* Tools for printing of Cases                                              *)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 5c0f42852d..8bbf48d59b 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -17,6 +17,7 @@ open Termops
 open Sign
 open Environ
 open Libnames
+open Mod_subst
 
 (* The type of mappings for existential variables *)
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 9f10d2dfe8..fff6808d19 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -14,6 +14,7 @@ open Names
 open Term
 open Sign
 open Libnames
+open Mod_subst
 (*i*)
 
 (* The type of mappings for existential variables.
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 5cb07e219a..243da5cc1b 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -17,6 +17,7 @@ open Rawterm
 open Environ
 open Nametab
 open Pp
+open Mod_subst
 
 (* Metavariables *)
 
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 3d2bd72149..3981173030 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -17,6 +17,7 @@ open Environ
 open Libnames
 open Nametab
 open Rawterm
+open Mod_subst
 (*i*)
 
 (* Pattern variables *)
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index d93a583c40..48b41444eb 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -16,6 +16,7 @@ open Term
 open Libnames
 open Nametab
 open Evd
+open Mod_subst
 (*i*)
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 7e8b8b8949..0a582ef7bb 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -15,6 +15,7 @@ open Sign
 open Term
 open Libnames
 open Nametab
+open Mod_subst
 (*i*)
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
@@ -99,7 +100,7 @@ val occur_rawconstr : identifier -> rawconstr -> bool
 
 val loc_of_rawconstr : rawconstr -> loc
 
-val subst_raw : Names.substitution -> rawconstr -> rawconstr
+val subst_raw : substitution -> rawconstr -> rawconstr
 
 type 'a raw_red_flag = {
   rBeta : bool;
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 6d7921f0d4..64d99d49fb 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -19,6 +19,7 @@ open Typeops
 open Libobject
 open Library
 open Classops
+open Mod_subst
 
 (*s Une structure S est un type inductif non récursif à un seul
    constructeur (de nom par défaut Build_S) *)