X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguator.ml;h=05c988ac16c98b349fed54a0a4c7268e3bcdb2de;hb=5929e58cedcbdc70ce429aae939219ce7555d953;hp=d9de808b019ea796235e551e4c33a591453f02f1;hpb=8f9d476c32c48d14348a61889dc191c7696bd404;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
index d9de808b0..05c988ac1 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
@@ -75,6 +75,8 @@ module Disambiguator = Disambiguate.Make (Callbacks)
 
 (* implement module's API *)
 
+let only_one_pass = ref false;;
+
 let disambiguate_thing ~aliases ~universe
   ~(f:?fresh_instances:bool ->
       aliases:DisambiguateTypes.environment ->
@@ -88,7 +90,10 @@ let disambiguate_thing ~aliases ~universe
   let library = false, DisambiguateTypes.Environment.empty, None in
   let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
   let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
-  let passes =  (* <fresh_instances?, aliases, coercions?> *)
+  let passes = (* <fresh_instances?, aliases, coercions?> *)
+   if !only_one_pass then
+    [ (false, mono_aliases, false) ]
+   else
     [ (false, mono_aliases, false);
       (false, multi_aliases, false);
       (true, mono_aliases, false);