X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicSubstitution.ml;h=4f5e25ecce91be0764fc841ee5bf423bdea7a317;hb=3594cdffdc6941ed86fef264a681e5db417c5d8a;hp=67bada94989b41a4631158f3f3abd18a190a1541;hpb=b7387e01fb1ce2745a6df6ffc254dba7d13d35ac;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml
index 67bada949..4f5e25ecc 100644
--- a/helm/software/components/ng_kernel/nCicSubstitution.ml
+++ b/helm/software/components/ng_kernel/nCicSubstitution.ml
@@ -64,6 +64,8 @@ let lift ?(from=1) n t =
 let rec psubst ?(avoid_beta_redexes=false) delift lift_args args = 
  let nargs = List.length args in
  let rec substaux k = function
+    | NCic.Sort _ 
+    | NCic.Const _ as t -> t
     | NCic.Rel n as t ->
        (match n with
        | n when n >= (k+nargs) -> if delift then NCic.Rel (n - nargs) else t
@@ -78,7 +80,6 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args args =
        (* 1-nargs < k-m, when <= 0 is still reasonable because we will
         * substitute args[ k-m ... k-m+nargs-1 > 0 ] *)
        NCic.Meta (i,(m, NCic.Ctx (List.map (substaux (k-m)) lctx)))
-    | NCic.Sort _ as t -> t
     | NCic.Implicit _ -> assert false (* was identity *)
     | NCic.Prod (n,s,t) -> NCic.Prod (n, substaux k s, substaux (k + 1) t)
     | NCic.Lambda (n,s,t) -> NCic.Lambda (n, substaux k s, substaux (k + 1) t)
@@ -98,7 +99,6 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args args =
        let tl = List.map (substaux k) tl in
        avoid (substaux k he) tl
     | NCic.Appl _ -> assert false
-    | NCic.Const _ as t -> t
     | NCic.Match (r,outt,t,pl) ->
        NCic.Match (r,substaux k outt, substaux k t, List.map (substaux k) pl)
  in