matitaprover

[helm.git] / components / tactics / paramodulation / subst.ml

diff --git a/components/tactics/paramodulation/subst.ml b/components/tactics/paramodulation/subst.ml
index f738d2f63354a343c82b0416d5cd6cb69f7e3ded..7e8ab8b185235b30a5e8a5aaef29ece17752ee5d 100644 (file)
--- a/components/tactics/paramodulation/subst.ml
+++ b/components/tactics/paramodulation/subst.ml
@@ -76,7 +76,7 @@ let cic_merge_subst_if_possible s1 s2 =
 
 type naif_substitution = (int * Cic.term) list 
 
-let naif_apply_subst subst term =
+let naif_apply_subst lift subst term =
  let rec aux k t =
    match t with
        Cic.Rel _ -> t
@@ -87,7 +87,7 @@ let naif_apply_subst subst term =
            Cic.Var (uri, exp_named_subst')
     | Cic.Meta (i, l) -> 
         (try
-          aux k (CicSubstitution.lift k (List.assoc i subst)) 
+          aux k (CicSubstitution.lift (k+lift) (List.assoc i subst)) 
          with Not_found -> t)
     | Cic.Sort _
     | Cic.Implicit _ -> t
@@ -141,7 +141,7 @@ substitution to the context *)
 let naif_apply_subst_metasenv subst metasenv =
   List.map
     (fun (n, context, ty) ->
-      (n, context, naif_apply_subst subst ty))
+      (n, context, naif_apply_subst 0 subst ty))
     (List.filter
       (fun (i, _, _) -> not (List.mem_assoc i subst))
       metasenv)
@@ -157,7 +157,7 @@ let naif_ppsubst names subst =
 let naif_buildsubst n context t ty tail = (n,t) :: tail ;;
 
 let naif_flatten_subst subst = 
-  List.map (fun (i,t) -> i, naif_apply_subst subst t ) subst
+  List.map (fun (i,t) -> i, naif_apply_subst 0 subst t ) subst
 ;;
 
 let rec naif_lookup_subst meta subst =
@@ -189,7 +189,8 @@ let naif_merge_subst_if_possible s1 s2 =
 (********** ACTUAL SUBSTITUTION IMPLEMENTATION *******************************)
 
 type substitution = naif_substitution
-let apply_subst = naif_apply_subst
+let apply_subst = naif_apply_subst 0
+let apply_subst_lift = naif_apply_subst
 let apply_subst_metasenv = naif_apply_subst_metasenv
 let ppsubst ?(names=[]) l = naif_ppsubst names l
 let buildsubst = naif_buildsubst
@@ -211,5 +212,6 @@ let merge_subst_if_possible = naif_merge_subst_if_possible;;
 
 let empty_subst = [];;
 
-let concat_substs x y = x @ y;;
+let concat x y = x @ y;;
+