Removed two args from psubst.

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 5a8ba41648d861928bf223bf22a43b105f3f3be0..99afc2aa8b27ad0822822480cafa9a730faa366f 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -351,7 +351,7 @@ module Reduction(RS : Strategy) =
       if k = 0 then t 
       else 
         NCicSubstitution.psubst ~avoid_beta_redexes:true  
-          true 0 (RS.from_env_for_unwind ~unwind) e t
+          (RS.from_env_for_unwind ~unwind) e t
     in
     if s = [] then t 
     else NCic.Appl(t::(RS.from_stack_list_for_unwind ~unwind s))

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml
index 51e4244c0073a1f67e405bd752fa29c4a50f0a64..11d17de32827ee7dbfeefcba47bb9ee8ed24cf1a 100644 (file)
--- a/helm/software/components/ng_kernel/nCicSubstitution.ml
+++ b/helm/software/components/ng_kernel/nCicSubstitution.ml
@@ -40,21 +40,21 @@ let lift ?(from=1) n t =
 (*  well typed and avoid_beta_redexes is true.                          *)
 (*  map_arg is ReductionStrategy.from_env_for_unwind when psubst is     *)
 (*  used to implement nCicReduction.unwind'                             *)
-let rec psubst ?(avoid_beta_redexes=false) delift lift_args map_arg args = 
+let rec psubst ?(avoid_beta_redexes=false) map_arg args = 
  let nargs = List.length args in
  let rec substaux k = function
    | NCic.Rel n as t ->
       (match n with
       | n when n >= (k+nargs) ->
-         if delift && nargs <> 0 then NCic.Rel (n - nargs) else t
+         if nargs <> 0 then NCic.Rel (n - nargs) else t
       | n when n < k -> t
       | n (* k <= n < k+nargs *) ->
-       (try lift (k-1+lift_args) (map_arg (List.nth args (n-k)))
+       (try lift (k-1) (map_arg (List.nth args (n-k)))
         with Failure _ -> assert false))
    | NCic.Meta (i,(m,l)) as t when m >= k + nargs - 1 -> 
-       if delift && nargs <> 0 then NCic.Meta (i,(m-nargs,l)) else t
+       if nargs <> 0 then NCic.Meta (i,(m-nargs,l)) else t
    | NCic.Meta (i,(m,(NCic.Irl l as irl))) as t when k > l + m -> 
-       if delift && nargs <> 0 then NCic.Meta (i,(m-nargs,irl)) else t
+       if nargs <> 0 then NCic.Meta (i,(m-nargs,irl)) else t
    | NCic.Meta (i,(m,l)) -> 
       let lctx = NCicUtils.expand_local_context l in
       (* 1-nargs < k-m, when <= 0 is still reasonable because we will
@@ -72,7 +72,7 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args map_arg args =
                 (* map_arg is here \x.x, Obj magic is needed because 
                  * we don't have polymorphic recursion w/o records *)
                 avoid (psubst 
-                  ~avoid_beta_redexes true 0 Obj.magic [Obj.magic arg] bo) tl'
+                  ~avoid_beta_redexes Obj.magic [Obj.magic arg] bo) tl'
             | _ -> if he == he' && args == tl then t else NCic.Appl (he'::args))
       in
       let tl = HExtlib.sharing_map (substaux k) tl in
@@ -83,14 +83,14 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args map_arg args =
 ;;
 
 let subst ?avoid_beta_redexes arg = 
-  psubst ?avoid_beta_redexes true 0 (fun x -> x)[arg];;
+  psubst ?avoid_beta_redexes (fun x -> x)[arg];;
 
 (* subst_meta (n, Some [t_1 ; ... ; t_n]) t                                  *)
 (*  returns the term [t] where [Rel i] is substituted with [t_i] lifted by n *)
 (*  [t_i] is lifted as usual when it crosses an abstraction                  *)
-(* subst_meta (n, Non) t -> lift n t                                        *)
+(* subst_meta (n, Non) t -> lift n t                                         *)
 let subst_meta = function 
   | m, NCic.Irl _ 
   | m, NCic.Ctx [] -> lift m 
-  | m, NCic.Ctx l  -> psubst false m (fun x -> x) l 
+  | m, NCic.Ctx l  -> psubst (lift m) l 
 ;;

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.mli b/helm/software/components/ng_kernel/nCicSubstitution.mli
index 7e3301fa8ec037135215662c955bfe58f68978d8..9b277078d4b892729325084dc335819cc6a2f836 100644 (file)
--- a/helm/software/components/ng_kernel/nCicSubstitution.mli
+++ b/helm/software/components/ng_kernel/nCicSubstitution.mli
@@ -35,7 +35,7 @@ val subst : ?avoid_beta_redexes:bool -> NCic.term -> NCic.term -> NCic.term
  *    the function is ReductionStrategy.from_env_for_unwind when psubst is
  *    used to implement nCicReduction.unwind'                              *)
 val psubst : 
-  ?avoid_beta_redexes:bool -> bool -> int -> 
+  ?avoid_beta_redexes:bool ->  
   ('a -> NCic.term) -> 'a list -> NCic.term -> 
     NCic.term