X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.ml;fp=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.ml;h=f312f556c9600fc3ea1179df2d1e54f72ee3867a;hb=c929e791b0eca1e75694a663a2f6ada9f0ff9534;hp=ae51f35803e20cfd6467b54983afbe6b0dd5747d;hpb=a38dce333847f6a1eaed563f7a2260e1cfc1ff2e;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index ae51f3580..f312f556c 100644
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -53,7 +53,6 @@ let lift n =
     | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
     | C.Appl l -> C.Appl (List.map (liftaux k) l)
     | C.Const _ as t -> t
-    | C.Abst _  as t -> t
     | C.MutInd _ as t -> t
     | C.MutConstruct _ as t -> t
     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
@@ -118,7 +117,6 @@ let subst arg =
         end
     | C.Appl _ -> assert false
     | C.Const _ as t -> t
-    | C.Abst _ as t -> t
     | C.MutInd _ as t -> t
     | C.MutConstruct _ as t -> t
     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
@@ -208,7 +206,6 @@ let lift_meta l t =
     | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t)
     | C.Appl l -> C.Appl (List.map (aux k) l)
     | C.Const _ as t -> t
-    | C.Abst _ as t -> t
     | C.MutInd _ as t -> t
     | C.MutConstruct _ as t -> t
     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->