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

5 files changed, 16 insertions, 11 deletions

diff --git a/parsing/ast.mli b/parsing/ast.mli
index 28e8e132f2..b915c65523 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -16,6 +16,7 @@ open Libnames
 open Coqast
 open Topconstr
 open Genarg
+open Mod_subst
 (*i*)
 
 (* Abstract syntax trees. *)
@@ -120,4 +121,4 @@ val first_matchl : ('a -> patlist) -> env -> Coqast.t list -> 'a list ->
 val to_pat : entry_env -> Coqast.t -> (astpat * entry_env)
 
 (* Object substitution in modules *)
-val subst_astpat : Names.substitution -> astpat -> astpat
+val subst_astpat : substitution -> astpat -> astpat
diff --git a/parsing/coqast.ml b/parsing/coqast.ml
index 52681fe342..a80982f8ac 100644
--- a/parsing/coqast.ml
+++ b/parsing/coqast.ml
@@ -12,6 +12,7 @@
 open Util
 open Names
 open Libnames
+open Mod_subst
 (*i*)
 
 type t =
@@ -116,11 +117,11 @@ let rec subst_ast subst ast = match ast with
 	if ast1' == ast1 then ast else
 	  Smetalam (l,s,ast1')
   | Path (loc,kn) -> 
-      let kn' = Names.subst_kn subst kn in
+      let kn' = subst_kn subst kn in
 	if kn' == kn then ast else
 	  Path(loc,kn')
   | ConPath (loc,kn) -> 
-      let kn' = Names.subst_con subst kn in
+      let kn' = subst_con subst kn in
 	if kn' == kn then ast else
 	  ConPath(loc,kn')
   | Nmeta _
diff --git a/parsing/coqast.mli b/parsing/coqast.mli
index fcb029319c..a769c66f96 100644
--- a/parsing/coqast.mli
+++ b/parsing/coqast.mli
@@ -12,6 +12,7 @@
 open Util
 open Names
 open Libnames
+open Mod_subst
 (*i*)
 
 (* Abstract syntax trees. *)
@@ -42,7 +43,7 @@ val hcons_ast:
   * (kernel_name -> kernel_name) * (constant -> constant)
   -> (t -> t) * (loc -> loc)
 
-val subst_ast: Names.substitution -> t -> t
+val subst_ast: substitution -> t -> t
 
 (*
 val map_tactic_expr : (t -> t) -> (tactic_expr -> tactic_expr) -> tactic_expr -> tactic_expr
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 58a889348c..b6844e5476 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -16,6 +16,7 @@ open Coqast
 open Vernacexpr
 open Extend
 open Rawterm
+open Mod_subst
 (*i*)
 
 type all_grammar_command =
@@ -48,7 +49,7 @@ val get_extend_vernac_grammars :
 val reset_extend_grammars_v8 : unit -> unit
 
 val subst_all_grammar_command :
-  Names.substitution -> all_grammar_command -> all_grammar_command
+  substitution -> all_grammar_command -> all_grammar_command
 
 val interp_entry_name : string -> string -> 
   entry_type * Token.t Gramext.g_symbol
diff --git a/parsing/extend.mli b/parsing/extend.mli
index d8f0827db6..c9558a970c 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -17,6 +17,7 @@ open Coqast
 open Ppextend
 open Topconstr
 open Genarg
+open Mod_subst
 (*i*)
 
 type entry_type = argument_type
@@ -98,7 +99,7 @@ val rename_command_entry : string -> string
 val explicitize_entry : string -> string -> constr_entry
 
 val subst_grammar_command : 
-  Names.substitution -> grammar_command -> grammar_command
+  substitution -> grammar_command -> grammar_command
 
 (* unparsing objects *)
 
@@ -113,7 +114,7 @@ type 'pat unparsing_hunk =
   | UNP_SYMBOLIC of string option * string * 'pat unparsing_hunk
 
 (*val subst_unparsing_hunk : 
-  Names.substitution -> (Names.substitution -> 'pat -> 'pat) -> 
+  substitution -> (substitution -> 'pat -> 'pat) -> 
   'pat unparsing_hunk -> 'pat unparsing_hunk
 *)
 
@@ -130,8 +131,8 @@ type 'pat syntax_entry = {
   syn_hunks : 'pat unparsing_hunk list }
 
 val subst_syntax_entry : 
-  (Names.substitution -> 'pat -> 'pat) -> 
-  Names.substitution -> 'pat syntax_entry -> 'pat syntax_entry
+  (substitution -> 'pat -> 'pat) -> 
+  substitution -> 'pat syntax_entry -> 'pat syntax_entry
 
 
 type 'pat syntax_command = { 
@@ -139,8 +140,8 @@ type 'pat syntax_command = {
   sc_entries : 'pat syntax_entry list }
 
 val subst_syntax_command : 
-  (Names.substitution -> 'pat -> 'pat) -> 
-  Names.substitution -> 'pat syntax_command -> 'pat syntax_command
+  (substitution -> 'pat -> 'pat) -> 
+  substitution -> 'pat syntax_command -> 'pat syntax_command
 
 type syntax_rule = string * Coqast.t * Coqast.t unparsing_hunk list
 type raw_syntax_entry = precedence * syntax_rule list