New command "inverter" used to generate an induction/inversion principle for

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

diff --git a/helm/software/components/tactics/paramodulation/subst.ml b/helm/software/components/tactics/paramodulation/subst.ml
index 819472a15485c0314da6228a3374f300d67d7e94..fb8e3b78e25266a473fc3d0d9b9f5d59ce7a06e7 100644 (file)
--- a/helm/software/components/tactics/paramodulation/subst.ml
+++ b/helm/software/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,14 +87,14 @@ 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
     | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
     | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
     | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
-    | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
+    | Cic.LetIn (n,s,ty,t) -> Cic.LetIn (n, aux k s, aux k ty, aux (k+1) t)
     | Cic.Appl [] -> assert false
     | Cic.Appl l -> Cic.Appl (List.map (aux k) l)
     | Cic.Const (uri,exp_named_subst) ->
@@ -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