X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=570ab894e434e7b9f45b5444e854c14b09fda6fe;hb=a6dd077a2b3e4d0c4395c2ee4cc2e1b6d10ab963;hp=54478c81a795862a8c89349a010ccd8ce954f5ae;hpb=d8dd9228da904dd64317ef87e0f1b499af8606ba;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 54478c81a..570ab894e 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -73,9 +73,6 @@ let refine metasenv context term ugraph =
           debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
             (CicPp.ppterm term) msg);
           Ko,ugraph
-      | CicUnification.UnificationFailure s -> 
-	 prerr_endline ("PASSADI QUI: " ^ s);
-	   raise ( CicUnification.UnificationFailure s )
 
 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
   try
@@ -417,6 +414,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 +461,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 +638,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