* Abst removed from the DTD

[helm.git] / helm / gTopLevel / proofEngine.ml

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index f33c69e35918cd64ef4a3b2527230a2490ab6609..c605d41a97d2848eca8fd05c4575d8e8aa46d184 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -133,7 +133,6 @@ let metas_in_term term =
     | C.LetIn (_,s,t) -> (aux s) @ (aux t)
     | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
     | C.Const _
-    | C.Abst _
     | C.MutInd _
     | C.MutConstruct _ -> []
     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
@@ -450,7 +449,6 @@ let eta_expand metasenv context t arg =
     | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
     | C.Appl l -> C.Appl (List.map (aux n) l)
     | C.Const _ as t -> t
-    | C.Abst _ -> assert false
     | C.MutInd _
     | C.MutConstruct _ as t -> t
     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
@@ -579,6 +577,7 @@ let elim_intros_simpl term =
                  | _ ->raise NotTheRightEliminatorShape
                in
                 find_head he,fargs
+            | C.Meta (emeta,_) -> emeta,[]
 (* *)
             | _ -> raise NotTheRightEliminatorShape
           in