X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteDisambiguator.ml;h=181532462b7b370140297ee48a119e7510e30991;hb=61acdea2419b3889096fd1e41275062b78253af0;hp=d9de808b019ea796235e551e4c33a591453f02f1;hpb=cbcd34fe15122eb9835a5226b98be1050b097d6a;p=helm.git

diff --git a/components/grafite_parser/grafiteDisambiguator.ml b/components/grafite_parser/grafiteDisambiguator.ml
index d9de808b0..181532462 100644
--- a/components/grafite_parser/grafiteDisambiguator.ml
+++ b/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,10 +90,11 @@ 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?> *)
-    [ (false, mono_aliases, false);
-      (false, multi_aliases, false);
-      (true, mono_aliases, false);
+  let passes = (* <fresh_instances?, aliases, coercions?> *)
+   if !only_one_pass then
+    [ (true, mono_aliases, false) ]
+   else
+    [ (true, mono_aliases, false);
       (true, multi_aliases, false);
       (true, mono_aliases, true);
       (true, multi_aliases, true);
@@ -105,16 +108,17 @@ let disambiguate_thing ~aliases ~universe
     f ~fresh_instances ~aliases ~universe thing
   in
   let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
-   if use_mono_aliases && not instances then
-    drop_aliases res
+   if use_mono_aliases then
+    drop_aliases ~minimize_instances:true res (* one shot aliases *)
    else if user_asked then
     drop_aliases ~minimize_instances:true res (* one shot aliases *)
    else
     drop_aliases_and_clear_diff res
   in
-  let rec aux errors =
-    function
-    | [ pass ] ->
+  let rec aux i errors passes =
+(*prerr_endline ("Pass: " ^ string_of_int i);*)
+   match passes with
+      [ pass ] ->
         (try
           set_aliases pass (try_pass pass)
          with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
@@ -123,12 +127,12 @@ let disambiguate_thing ~aliases ~universe
         (try
           set_aliases hd (try_pass hd)
         with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) ->
-         aux (errors @ [newerrors]) tl)
+         aux (i+1) (errors @ [newerrors]) tl)
     | [] -> assert false
   in
   let saved_insert_coercions = !CicRefine.insert_coercions in
   try
-    let res = aux [] passes in
+    let res = aux 1 [] passes in
     CicRefine.insert_coercions := saved_insert_coercions;
     res
   with exn ->