]> matita.cs.unibo.it Git - helm.git/commitdiff
bugfix when user query contains metas: their context should not be analyzed
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 15 Mar 2005 08:21:56 +0000 (08:21 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 15 Mar 2005 08:21:56 +0000 (08:21 +0000)
as it were in main position

helm/ocaml/metadata/metadataExtractor.ml

index d06e9a4bf5197b0da61bc34efe335e984222bfc3..8db0d74f5e47ef15b808025f14388981ec10924a 100644 (file)
@@ -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 ->