merged changes from the svn fork by me and Enrico

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

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 54478c81a795862a8c89349a010ccd8ce954f5ae..552e3d30b21898eb7596194b6a7c3f7d4c263d8f 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -417,6 +417,21 @@ let domain_diff dom1 dom2 =
   in
   List.filter (fun elt -> not (is_in_dom2 elt)) dom1
 
+module type Disambiguator =
+sig
+  val disambiguate_term :
+    dbd:Mysql.dbd ->
+    context:Cic.context ->
+    metasenv:Cic.metasenv ->
+    ?initial_ugraph:CicUniv.universe_graph -> 
+    aliases:environment ->  (* previous interpretation status *)
+    CicAst.term ->
+    (environment *                   (* new interpretation status *)
+     Cic.metasenv *                  (* new metasenv *)
+     Cic.term*
+     CicUniv.universe_graph) list    (* disambiguated term *)
+end
+
 module Make (C: Callbacks) =
   struct
     let choices_of_id dbd id =
@@ -449,8 +464,9 @@ module Make (C: Callbacks) =
            fun _ _ _ -> term))
         uris
 
-    let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term
+    let disambiguate_term ~(dbd:Mysql.dbd) ~context ~metasenv
       ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
+      term
     =
       debug_print "NEW DISAMBIGUATE INPUT";
       let disambiguate_context =  (* cic context -> disambiguate context *)
@@ -625,8 +641,8 @@ struct
         ?(aliases=DisambiguateTypes.Environment.empty) term =
     let ast = CicTextualParser2.parse_term (Stream.of_string term) in
     try
-      Disambiguator.disambiguate_term ~dbd context metasenv ast ?initial_ugraph
-        ~aliases
+      Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
+        ?initial_ugraph ~aliases
     with Exit -> raise (Ambiguous_term term)
 end