X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=7510c1cc59f1bb61b7b310fb1c33561d6527a3ce;hb=5c92c318030a05c766b3f6070dbd23589cbdee04;hp=28742e6c7651c93edc8cd9a423bed51df0da2139;hpb=52a0d6251f26055df769b179641fe077046e1f09;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 28742e6c7..7510c1cc5 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -43,7 +43,7 @@ let singleton msg = function
          Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
          msg (List.length l)
       in
-      HLog.debug debug; assert false
+      prerr_endline debug; assert false
 
 let __Implicit = "__Implicit__"
 let __Closed_Implicit = "__Closed_Implicit__"
@@ -307,15 +307,18 @@ let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
 ;;
 
 let disambiguate_auto_params 
-  disambiguate_term metasenv context (terms, params) 
+  disambiguate_term metasenv context (oterms, params) 
 =
-    let metasenv, terms = 
-      List.fold_right 
-       (fun t (metasenv, terms) ->
-         let metasenv,t = disambiguate_term context metasenv t in
-         metasenv,t::terms) terms (metasenv, [])
-    in
-    metasenv, (terms, params)
+  match oterms with 
+    | None -> metasenv, (None, params)
+    | Some terms ->
+	let metasenv, terms = 
+	  List.fold_right 
+	    (fun t (metasenv, terms) ->
+               let metasenv,t = disambiguate_term context metasenv t in
+		 metasenv,t::terms) terms (metasenv, [])
+	in
+	  metasenv, (Some terms, params)
 ;;
 
 let disambiguate_just disambiguate_term context metasenv =