* Abst removed from the DTD

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

diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml
index 0cf33c83cc155bff55f1abd37db3146422b35e07..2812bd64e02f352c824c17d0bb3eb8260f594bbe 100644 (file)
--- a/helm/gTopLevel/mquery.ml
+++ b/helm/gTopLevel/mquery.ml
@@ -187,7 +187,6 @@ let rec inspect_term main l v = function
    | Meta (i, _)                  -> l
    | Sort s                       -> l 
    | Implicit                     -> l 
-   | Abst u                       -> l 
    | Var u                        -> inspect_uri main l u None None v
    | Const (u, i)                 -> inspect_uri main l u None None v
    | MutInd (u, i, t)             -> inspect_uri main l u (Some t) None v