X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.mli;h=a2cc0d0e7b04489333cadfb33572aa9b60dfbb49;hb=99b249b23524cda2d91602ee088fef1a7be253ee;hp=356b5e117274f570634e15167c07ad810d76d2d5;hpb=259a4a2080cc5af5b20da1cd9133eb32f28c5d8f;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index 356b5e117..a2cc0d0e7 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -25,11 +25,13 @@
 
 (** {2 Disambiguation interface} *)
 
-exception NoWellTypedInterpretation
+(* the integer is an offset to be added to each location *)
+exception NoWellTypedInterpretation of
+ int * (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 =
@@ -45,7 +47,7 @@ sig
     ?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 *
@@ -59,7 +61,7 @@ sig
     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 +71,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:HMysql.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
-