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

6 files changed, 20 insertions, 14 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 45fc35d4b4..9bf5cc741d 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -39,6 +39,7 @@ open Library
 open Printer
 open Declarations
 open Tacexpr
+open Mod_subst
 
 (****************************************************************************)
 (*            The Type of Constructions Autotactic Hints                    *)
@@ -291,21 +292,21 @@ let cache_autohint (_,(local,name,hintlist)) = add_hint name hintlist
     let recalc_hint ((_,data) as hint) =
       match data.code with
 	| Res_pf (c,_) ->
-	    let c' = Term.subst_mps subst c in
+	    let c' = subst_mps subst c in
 	      if c==c' then hint else
 		make_apply_entry env sigma (false,false) 
 		  data.hname (c', type_of env sigma c')
 	| ERes_pf (c,_) ->
-	    let c' = Term.subst_mps subst c in
+	    let c' = subst_mps subst c in
 	      if c==c' then hint else
 		make_apply_entry env sigma (true,false) 
 		  data.hname (c', type_of env sigma c')
 	| Give_exact c ->
-	    let c' = Term.subst_mps subst c in
+	    let c' = subst_mps subst c in
 	      if c==c' then hint else
 		make_exact_entry data.hname (c',type_of env sigma c')
 	| Res_pf_THEN_trivial_fail (c,_) ->
-	    let c' = Term.subst_mps subst c in
+	    let c' = subst_mps subst c in
 	      if c==c' then hint else
 		make_trivial env sigma (data.hname,c')
 	| Unfold_nth ref -> 
@@ -335,19 +336,19 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) =
     let lab' = subst_label subst lab in
     let data' = match data.code with
       | Res_pf (c, clenv) ->
-	  let c' = Term.subst_mps subst c in
+	  let c' = subst_mps subst c in
 	    if c==c' then data else
 	      trans_data data (Res_pf (c', trans_clenv clenv))
       | ERes_pf (c, clenv) ->
-	  let c' = Term.subst_mps subst c in
+	  let c' = subst_mps subst c in
 	    if c==c' then data else
 	      trans_data data (ERes_pf (c', trans_clenv clenv))
       | Give_exact c ->
-	  let c' = Term.subst_mps subst c in
+	  let c' = subst_mps subst c in
 	    if c==c' then data else
 	      trans_data data (Give_exact c')
       | Res_pf_THEN_trivial_fail (c, clenv) ->
-	  let c' = Term.subst_mps subst c in
+	  let c' = subst_mps subst c in
 	    if c==c' then data else
 	      let code' = Res_pf_THEN_trivial_fail (c', trans_clenv clenv) in
 		trans_data data code'
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 950e272bc4..68a8a3ba92 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -21,6 +21,7 @@ open Environ
 open Evd
 open Libnames
 open Vernacexpr
+open Mod_subst
 (*i*)
   
 type auto_tactic = 
@@ -126,7 +127,7 @@ val set_extern_intern_tac :
   -> unit
 
 val set_extern_subst_tactic :
-  (Names.substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr)
+  (substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr)
   -> unit
 
 (* Create a Hint database from the pairs (name, constr).
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 6b6536ec43..addf30bc4d 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -20,6 +20,7 @@ open Term
 open Util
 open Vernacinterp
 open Tacexpr
+open Mod_subst
 
 (* Rewriting rules *)
 (* the type is the statement of the lemma constr. Used to elim duplicates. *)
@@ -88,7 +89,7 @@ let export_hintrewrite x = Some x
 
 let subst_hintrewrite (_,subst,(rbase,list as node)) = 
   let subst_first (cst,typ,b,t as pair) = 
-    let cst' = Term.subst_mps subst cst in
+    let cst' = subst_mps subst cst in
     let typ' =
      (* here we do not have the environment and Global.env () is not the
         one where cst' lives in. Thus we can just put a dummy value and
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index e278ec2433..f25687391c 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -31,6 +31,7 @@ open Safe_typing
 open Nametab
 open Decl_kinds
 open Constrintern
+open Mod_subst
 
 let replace = ref (fun _ _ -> assert false)
 let register_replace f = replace := f
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d447a97e85..5a33f89f3f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -41,6 +41,7 @@ open Typing
 open Hiddentac
 open Genarg
 open Decl_kinds
+open Mod_subst
 
 let strip_meta id = (* For Grammar v7 compatibility *)
   let s = string_of_id id in
@@ -312,7 +313,7 @@ type interp_genarg_type =
   (glob_sign -> raw_generic_argument -> glob_generic_argument) *
   (interp_sign -> goal sigma -> glob_generic_argument -> 
     closed_generic_argument) *
-  (Names.substitution -> glob_generic_argument -> glob_generic_argument)
+  (substitution -> glob_generic_argument -> glob_generic_argument)
 
 let extragenargtab =
   ref (Gmap.empty : (string,interp_genarg_type) Gmap.t)
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index f12960358c..8d8d12fb40 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -19,6 +19,7 @@ open Term
 open Tacexpr
 open Genarg
 open Topconstr
+open Mod_subst
 (*i*)
 
 (* Values for interpretation *)
@@ -78,7 +79,7 @@ val add_interp_genarg :
     (glob_sign -> raw_generic_argument -> glob_generic_argument) *
     (interp_sign -> goal sigma -> glob_generic_argument -> 
       closed_generic_argument) *
-    (Names.substitution -> glob_generic_argument -> glob_generic_argument)
+    (substitution -> glob_generic_argument -> glob_generic_argument)
     -> unit
 
 val interp_genarg :
@@ -94,10 +95,10 @@ val intern_hyp :
   glob_sign -> identifier Util.located -> identifier Util.located
 
 val subst_genarg :
-  Names.substitution -> glob_generic_argument -> glob_generic_argument
+  substitution -> glob_generic_argument -> glob_generic_argument
 
 val subst_rawconstr :
-  Names.substitution -> rawconstr_and_expr -> rawconstr_and_expr
+  substitution -> rawconstr_and_expr -> rawconstr_and_expr
 
 (* Interprets any expression *)
 val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value