From 30111ae182e35dc2f7aac9ea23746ba671d2001b Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 13 Oct 2008 15:53:15 +0000
Subject: [PATCH] bug in psubst fixed inside local context in Irl form

---
 .../components/ng_kernel/nCicSubstitution.ml        | 13 +++++++++----
 .../components/ng_kernel/nCicSubstitution.mli       |  6 ++++++
 2 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml
index 240dd0b27..93268e258 100644
--- 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 f470b8a4d..38408fe13 100644
--- 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]                       *)
-- 
2.39.2