bugfix when user query contains metas: their context should not be analyzed

[helm.git] / helm / ocaml / metadata / metadataExtractor.ml

diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml
index d06e9a4bf5197b0da61bc34efe335e984222bfc3..8db0d74f5e47ef15b808025f14388981ec10924a 100644 (file)
--- 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 ->