From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 15 Mar 2005 08:21:56 +0000 (+0000)
Subject: bugfix when user query contains metas: their context should not be analyzed
X-Git-Tag: old_htmls~5
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=74682761ea8bf251be5b599e3ac28ec0d95f0958;p=helm.git

bugfix when user query contains metas: their context should not be analyzed
as it were in main position
---

diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml
index d06e9a4bf..8db0d74f5 100644
--- a/helm/ocaml/metadata/metadataExtractor.ml
+++ b/helm/ocaml/metadata/metadataExtractor.ml
@@ -80,7 +80,7 @@ let compute_term pos term =
           (fun set context ->
             match context with
             | None -> set
-            | Some term -> aux pos set term)
+            | Some term -> aux (next_pos pos) set term)
           set
           local_context
     | Cic.Sort sort ->