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

diff --git a/helm/ocaml/cic_proof_checking/cicMiniReduction.ml b/helm/ocaml/cic_proof_checking/cicMiniReduction.ml
index cb5875f73..bdc6e3a09 100644
--- a/helm/ocaml/cic_proof_checking/cicMiniReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicMiniReduction.ml
@@ -37,7 +37,6 @@ let rec letin_nf =
    | C.LetIn (n,s,t) -> CicSubstitution.subst (letin_nf s) t
    | C.Appl l -> C.Appl (List.map letin_nf 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) ->