added Trivial module with a disambiguate_term implementation which took

[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 b0fe0fcd3e7dfa11f4a874d998971b198f2f14d2..4db990283b919825430810a363e28d5e0e390dda 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -44,3 +44,23 @@ module Make (C : Callbacks) :
        CicUniv.universe_graph) list    (* disambiguated term *)
   end
 
+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 ->
+    Cic.context ->
+    Cic.metasenv ->
+    ?initial_ugraph:CicUniv.universe_graph -> 
+    ?aliases:environment ->         (* previous interpretation status *)
+    string ->
+    (environment *                  (* new interpretation status *)
+     Cic.metasenv *                 (* new metasenv *)
+     Cic.term *
+     CicUniv.universe_graph) list   (* disambiguated term *)
+end
+