]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguate.mli
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.mli
index 356b5e117274f570634e15167c07ad810d76d2d5..e8d21c0cda5f98c57b74aa845a4e3e831217393f 100644 (file)
@@ -25,7 +25,7 @@
 
 (** {2 Disambiguation interface} *)
 
-exception NoWellTypedInterpretation
+exception NoWellTypedInterpretation of string Lazy.t list
 exception PathNotWellFormed
 
 val interpretate_path :
@@ -71,7 +71,7 @@ module Make (C : DisambiguateTypes.Callbacks) : Disambiguator
 
 module Trivial:
 sig
-  exception Ambiguous_term of string
+  exception Ambiguous_term of string Lazy.t
 
   (** disambiguate an _unanmbiguous_ term using dummy callbacks which fail if a
     * choice from the user is needed to disambiguate the term