Many many improvements:

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

diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml
index e9c50bd08be29e2e237d25e5f930aaeacc6a8d80..fb670923d4ab75a5f742dd94daaadcf625bddb5d 100644 (file)
--- a/helm/gTopLevel/mquery.ml
+++ b/helm/gTopLevel/mquery.ml
@@ -178,7 +178,7 @@ let inspect_uri main l uri t c =
 
 let rec inspect_term main l = function
    | Rel i                        -> l 
-   | Meta i                       -> l 
+   | Meta (i,_)                   -> l 
    | Sort s                       -> l 
    | Implicit                     -> l 
    | Abst u                       -> l