X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.mli;h=fc88b6cf84d54320fb092cb9a3f67763a1585897;hb=8d8ac4a42998970114e43c2fb13ff2c98f7c259a;hp=1c6d4bbe7d3e3002462b237a7b6b93aa36a5e736;hpb=2751c5d09df1148706c65de38a9a4946687d4589;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index 1c6d4bbe7..fc88b6cf8 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -25,11 +25,12 @@
 
 (** {2 Disambiguation interface} *)
 
-exception NoWellTypedInterpretation
+exception NoWellTypedInterpretation of
+ (Token.flocation option * string Lazy.t) list
 exception PathNotWellFormed
 
 val interpretate_path :
-  context:Cic.name list -> DisambiguateTypes.term ->
+  context:Cic.name list -> CicNotationPt.term ->
     Cic.term
 
 module type Disambiguator =
@@ -39,13 +40,13 @@ sig
    * input AST will be ignored. Defaults to false. *)
   val disambiguate_term :
     ?fresh_instances:bool ->
-    dbd:Mysql.dbd ->
+    dbd:HMysql.dbd ->
     context:Cic.context ->
     metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph -> 
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
-    DisambiguateTypes.term ->
+    CicNotationPt.term ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.term *
@@ -55,11 +56,11 @@ sig
   (** @param fresh_instances as per disambiguate_term *)
   val disambiguate_obj :
     ?fresh_instances:bool ->
-    dbd:Mysql.dbd ->
+    dbd:HMysql.dbd ->
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
-    GrafiteAst.obj ->
+    CicNotationPt.obj ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.obj *
@@ -69,23 +70,3 @@ end
 
 module Make (C : DisambiguateTypes.Callbacks) : Disambiguator
 
-module Trivial:
-sig
-  exception Ambiguous_term of string
-
-  (** disambiguate an _unanmbiguous_ term using dummy callbacks which fail if a
-    * choice from the user is needed to disambiguate the term
-    * @raise Ambiguous_term for ambiguous term *)
-  val disambiguate_string:
-    dbd:Mysql.dbd ->
-    ?context:Cic.context ->
-    ?metasenv:Cic.metasenv ->
-    ?initial_ugraph:CicUniv.universe_graph -> 
-    ?aliases:DisambiguateTypes.environment ->(* previous interpretation status*)
-    string ->
-    ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
-     Cic.metasenv *                 (* new metasenv *)
-     Cic.term *
-     CicUniv.universe_graph) list   (* disambiguated term *)
-end
-