X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=308144c21a6826e6a5d2952cdb24e977825a5e3e;hb=c3f967910eca5648fd69886166c66ddd49d92b54;hp=ca3bc0b90592bb623e5d1199903afadc6c39573e;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index ca3bc0b90..308144c21 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -36,16 +36,20 @@ type lazy_tactic =
   (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) 
     GrafiteAst.tactic
 
-let singleton = function
+let singleton msg = function
   | [x], _ -> x
-  | _ -> assert false
-;;
+  | l, _   ->
+      let debug = 
+         Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
+	 msg (List.length l)
+      in
+      HLog.debug debug; assert false
 
   (** @param term not meaningful when context is given *)
 let disambiguate_term text prefix_len lexicon_status_ref context metasenv term =
   let lexicon_status = !lexicon_status_ref in
   let (diff, metasenv, cic, _) =
-    singleton
+    singleton "first"
       (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
         ~aliases:lexicon_status.LexiconEngine.aliases
         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
@@ -65,7 +69,7 @@ let disambiguate_lazy_term text prefix_len lexicon_status_ref term =
   (fun context metasenv ugraph ->
     let lexicon_status = !lexicon_status_ref in
     let (diff, metasenv, cic, ugraph) =
-      singleton
+      singleton "second"
         (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
           ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
           ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
@@ -418,7 +422,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
     | CicNotationPt.Inductive _ -> assert false
     | CicNotationPt.Theorem _ -> None in
   let (diff, metasenv, cic, _) =
-    singleton
+    singleton "third"
       (GrafiteDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
         ~aliases:lexicon_status.LexiconEngine.aliases
         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri