X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=6aee803f42578cf16cb04a5187856470c2f3c48a;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=7510c1cc59f1bb61b7b310fb1c33561d6527a3ce;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 7510c1cc5..6aee803f4 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
-      prerr_endline debug; assert false
+      HLog.debug debug; assert false
 
 let __Implicit = "__Implicit__"
 let __Closed_Implicit = "__Closed_Implicit__"
@@ -81,18 +81,12 @@ let ncic_mk_choice = function
         ~term_of_nref:(fun nref -> NCic.Const nref)
        name dsc
   | LexiconAst.Number_alias (_, dsc) -> 
-     (try
-       let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
-        desc, `Num_interp
-         (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
-      with
-       DisambiguateChoices.Choice_not_found _ ->
-        let desc,f = DisambiguateChoices.lookup_num_by_dsc dsc in
-        desc, `Num_interp
+       let desc,f = DisambiguateChoices.lookup_num_by_dsc dsc in
+       desc, `Num_interp
          (fun num -> 
             fst (OCic2NCic.convert_term 
               (UriManager.uri_of_string "cic:/xxx/x.con") 
-              (match f with `Num_interp f -> f num | _ -> assert false))))
+              (match f with `Num_interp f -> f num | _ -> assert false)))
   | LexiconAst.Ident_alias (name, uri) -> 
      uri, `Sym_interp 
       (fun l->assert(l = []);
@@ -307,18 +301,15 @@ let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
 ;;
 
 let disambiguate_auto_params 
-  disambiguate_term metasenv context (oterms, params) 
+  disambiguate_term metasenv context (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 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)
 ;;
 
 let disambiguate_just disambiguate_term context metasenv =