X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=cd1e7aa0c18709714f0e5295f0a2f84dfa57bc40;hb=b1fb6b8e1767d775bc452303629e95941d142bea;hp=4a2cb243066b0a1b3efb0be2a7f88a54aaee65b4;hpb=0328c0e2938ce714d5d7358afdca00195577198e;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 4a2cb2430..cd1e7aa0c 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -104,7 +104,6 @@ let delift context metasenv l t =
      | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
      | C.Appl l -> C.Appl (List.map (deliftaux 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) ->
@@ -229,8 +228,6 @@ prerr_endline "<DELIFT2" ; flush stderr ;
 	    fo_unif_l subst metasenv (lr1, lr2) 
        | (C.Const _, _) 
        | (_, C.Const _)
-       | (C.Abst _, _) 
-       | (_, C.Abst _) 
        | (C.MutInd  _, _) 
        | (_, C.MutInd _)
        | (C.MutConstruct _, _)
@@ -335,7 +332,6 @@ CSCSCS
 	List.fold_left
 	  (function metasenv -> aux metasenv k) metasenv l
     | C.Const _
-    | C.Abst _
     | C.MutInd _ 
     | C.MutConstruct _ -> metasenv
     | C.MutCase (_,_,_,outty,t,pl) ->
@@ -447,7 +443,6 @@ prerr_endline "<DELIFT" ; flush stderr ;
         end
     | C.Appl _ -> assert false
     | C.Const _
-    | C.Abst _
     | C.MutInd _
     | C.MutConstruct _ as t -> t,metasenv
     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
@@ -542,7 +537,6 @@ let apply_subst_reducing subst meta_to_reduce t =
          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,outty,t,pl) ->