loc * lazy string -> (loc * string) lazy

[helm.git] / helm / software / components / ng_kernel / nCicSubstitution.ml

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml
index 240dd0b27622c7c669f57b23af04270a9c3b55ae..32fa33ac845b5a272bf233f3644082d61a33245a 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,14 @@ 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 (_,(m,(C.Irl l))) as t when k > l + m -> 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 *)