X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_proof_checking%2FcicCooking.ml;h=2c5d0b439ffbaebea810e836fe772828d5c88dba;hb=c5c48f3d3515f1dd95657245922ec1f340e17f70;hp=c382bb361f7e554ad56b6ce243a11f27a365bb6e;hpb=54b16bbdde9723382f555331916e2252e23e9bbb;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicCooking.ml b/helm/ocaml/cic_proof_checking/cicCooking.ml
index c382bb361..2c5d0b439 100644
--- a/helm/ocaml/cic_proof_checking/cicCooking.ml
+++ b/helm/ocaml/cic_proof_checking/cicCooking.ml
@@ -80,7 +80,6 @@ let cook curi cookingsno var is_letin =
           [C.Rel k])
        else
         C.Const (uri,UriManager.relative_depth curi uri cookingsno)
-    | C.Abst _ as t -> t
     | C.MutInd (uri,_,i) ->
        if not is_letin && match CicEnvironment.get_obj uri with
            C.InductiveDefinition (_,params,_) when mem var params -> true