X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.ml;h=f312f556c9600fc3ea1179df2d1e54f72ee3867a;hb=6f6b8f33397548319fef9b374f9e9017e7fa151d;hp=ae51f35803e20cfd6467b54983afbe6b0dd5747d;hpb=0328c0e2938ce714d5d7358afdca00195577198e;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) ->