]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_proof_checking/cicCooking.ml
Abst removed from the DTD.
[helm.git] / helm / ocaml / cic_proof_checking / cicCooking.ml
index c382bb361f7e554ad56b6ce243a11f27a365bb6e..2c5d0b439ffbaebea810e836fe772828d5c88dba 100644 (file)
@@ -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