The discriminate tactic accepts a term, not only an identifier!

[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 2f9bb97a5d799dacfc8c3251c457d3001c19f4c8..6b5e3f8332c60e21283486461032d020f12ac60d 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -230,7 +230,7 @@ let interpretate_term ~context ~env ~uri ~is_path ast =
           let cic =
             if is_uri ast then  (* we have the URI, build the term out of it *)
               try
-                CicUtil.term_of_uri name
+                CicUtil.term_of_uri (UriManager.uri_of_string name)
               with UriManager.IllFormedUri _ ->
                 CicTextualParser2.fail loc "Ill formed URI"
             else
@@ -622,7 +622,7 @@ module Make (C: Callbacks) =
       let uris =
        match uris with
         | [] ->
-           [UriManager.string_of_uri (C.input_or_locate_uri
+           [(C.input_or_locate_uri
             ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
         | [uri] -> [uri]
         | _ ->
@@ -635,12 +635,12 @@ module Make (C: Callbacks) =
       in
       List.map
         (fun uri ->
-          (uri,
+          (UriManager.string_of_uri uri,
            let term =
              try
                CicUtil.term_of_uri uri
              with exn ->
-               debug_print uri;
+               debug_print (UriManager.string_of_uri uri);
                debug_print (Printexc.to_string exn);
                assert false
             in