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

1 files changed, 0 insertions, 26 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 21ab2ea5d2..65bf7a565d 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -790,32 +790,6 @@ let substn_vars p vars =
 
 let subst_vars = substn_vars 1
 
-(* 
-map_kn : (kernel_name -> kernel_name) -> constr -> constr
-
-This should be rewritten to prevent duplication of constr's when not
-necessary.
-For now, it uses map_constr and is rather ineffective
-*)
-
-let rec map_kn f f_con c = 
-  let func = map_kn f f_con in
-    match kind_of_term c with
-      | Const kn -> 
-	  mkConst (f_con kn)
-      | Ind (kn,i) -> 
-	  mkInd (f kn,i)
-      | Construct ((kn,i),j) -> 
-	  mkConstruct ((f kn,i),j)
-      | Case (ci,p,c,l) ->
-	  let ci' = { ci with ci_ind = let (kn,i) = ci.ci_ind in f kn, i } in
-	  mkCase (ci', func p, func c, array_smartmap func l) 
-      | _ -> map_constr func c
-
-let subst_mps sub = 
-  map_kn (subst_kn sub) (subst_con sub)
-
-
 (*********************)
 (* Term constructors *)
 (*********************)