bug in psubst fixed inside local context in Irl form

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml
index 240dd0b27622c7c669f57b23af04270a9c3b55ae..93268e258049898d1156f85637a3e02f2ae65ecf 100644 (file)
--- a/helm/software/components/ng_kernel/nCicSubstitution.ml
+++ b/helm/software/components/ng_kernel/nCicSubstitution.ml
@@ -11,6 +11,12 @@
 
 (* $Id$ *)
 
+let ppterm = 
+  ref (fun ~context:_ ~subst:_ ~metasenv:_ ?inside_fix _ -> 
+       let _ = inside_fix in assert false)
+;;
+let set_ppterm f = ppterm := f;;
+
 module C = NCic 
 module Ref = NReference
 
@@ -53,16 +59,15 @@ let rec psubst ?(avoid_beta_redexes=false) map_arg args =
       | n when n < k -> t
       | n (* k <= n < k+nargs *) ->
        (try lift (k-1) (map_arg (List.nth args (n-k)))
-        with Failure _ -> assert false))
+        with Failure _ | Invalid_argument _ -> assert false))
    | C.Meta (i,(m,l)) as t when m >= k + nargs - 1 -> 
        if nargs <> 0 then C.Meta (i,(m-nargs,l)) else t
    | C.Meta (i,(m,(C.Irl l as irl))) as t when k > l + m -> 
        if nargs <> 0 then C.Meta (i,(m-nargs,irl)) else t
    | C.Meta (i,(m,l)) -> 
       let lctx = NCicUtils.expand_local_context l in
-      (* 1-nargs < k-m, when <= 0 is still reasonable because we will
-       * substitute args[ k-m ... k-m+nargs-1 > 0 ] *)
-      C.Meta (i,(m, C.Ctx (HExtlib.sharing_map (substaux (k-m)) lctx)))
+       C.Meta (i,(0, 
+         C.Ctx (HExtlib.sharing_map (fun x -> substaux k (lift m x)) lctx)))
    | C.Implicit _ -> assert false (* was identity *)
    | C.Appl (he::tl) as t ->
       (* Invariant: no Appl applied to another Appl *)

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.mli b/helm/software/components/ng_kernel/nCicSubstitution.mli
index f470b8a4de0aea8007da050116203c4192f49231..38408fe13203b10bda43ae7b46c2cde058348fdb 100644 (file)
--- a/helm/software/components/ng_kernel/nCicSubstitution.mli
+++ b/helm/software/components/ng_kernel/nCicSubstitution.mli
@@ -11,6 +11,12 @@
 
 (* $Id$ *)
 
+val set_ppterm : (context:NCic.context -> 
+  subst:NCic.substitution -> 
+  metasenv:NCic.metasenv ->
+  ?inside_fix:bool ->
+   NCic.term -> string) -> unit
+
 (* lift n t                                                              *)
 (*  lifts [t] of [n]                                                     *)
 (*  [from] default 1, lifts only indexes >= [from]                       *)