version 0.7.1

[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..62382c8975d328fae6b22ed6574851918008e584 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -119,7 +119,7 @@ let interpretate_term ~context ~env ~uri ~is_path ast =
         resolve env (Symbol (symb, i)) ~args:cic_args ()
     | CicAst.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
     | CicAst.Binder (binder_kind, (var, typ), body) ->
-        let cic_type = aux_option loc context typ in
+        let cic_type = aux_option loc context (Some `Type) typ in
         let cic_body = aux loc (var :: context) body in
         (match binder_kind with
         | `Lambda -> Cic.Lambda (var, cic_type, cic_body)
@@ -129,7 +129,7 @@ let interpretate_term ~context ~env ~uri ~is_path ast =
               ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ())
     | CicAst.Case (term, indty_ident, outtype, branches) ->
         let cic_term = aux loc context term in
-        let cic_outtype = aux_option loc context outtype in
+        let cic_outtype = aux_option loc context None outtype in
         let do_branch ((head, args), term) =
           let rec do_branch' context = function
             | [] -> aux loc context term
@@ -184,7 +184,7 @@ let interpretate_term ~context ~env ~uri ~is_path ast =
           List.map
             (fun ((name, typ), body, decr_idx) ->
               let cic_body = aux loc context' body in
-              let cic_type = aux_option loc context typ in
+              let cic_type = aux_option loc context (Some `Type) typ in
               let name =
                 match name with
                 | Cic.Anonymous ->
@@ -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
@@ -311,8 +311,8 @@ let interpretate_term ~context ~env ~uri ~is_path ast =
     | CicAst.Sort `CProp -> Cic.Sort Cic.CProp
     | CicAst.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
-  and aux_option loc context = function
-    | None -> Cic.Implicit (Some `Type)
+  and aux_option loc context annotation = function
+    | None -> Cic.Implicit annotation
     | Some term -> aux loc context term
   in
   match ast with
@@ -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