Abst removed from the DTD.

[helm.git] / helm / ocaml / cic_unification / cicUnification.ml

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 4a2cb243066b0a1b3efb0be2a7f88a54aaee65b4..cd1e7aa0c18709714f0e5295f0a2f84dfa57bc40 100644 (file)
--- 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) ->