Experimental localization of errors during refinement and disambiguation.

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.mli

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index 1c6d4bbe7d3e3002462b237a7b6b93aa36a5e736..fc88b6cf84d54320fb092cb9a3f67763a1585897 100644 (file)
--- 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
-