End of patch for computation of LetIn types. Now types of mutually (co)recursive

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index ca3bc0b90592bb623e5d1199903afadc6c39573e..dfaf5b42426816f6f3dcfed8c333dc4c5565726a 100644 (file)
--- 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)
@@ -99,7 +103,6 @@ let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
       let t = disambiguate_lazy_term text prefix_len lexicon_status_ref t in
       `Unfold (Some t)
   | `Normalize
-  | `Reduce
   | `Simpl
   | `Unfold None
   | `Whd as kind -> kind
@@ -418,7 +421,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