X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=62382c8975d328fae6b22ed6574851918008e584;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=27122ef1deaf635f594d2931d2a606046fc81069;hpb=a7b90d2494f7d580faa54ecd2835bd4649129763;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 27122ef1d..62382c897 100644
--- 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
@@ -638,7 +638,7 @@ module Make (C: Callbacks) =
           (UriManager.string_of_uri uri,
            let term =
              try
-               CicUtil.term_of_uri (UriManager.string_of_uri uri)
+               CicUtil.term_of_uri uri
              with exn ->
                debug_print (UriManager.string_of_uri uri);
                debug_print (Printexc.to_string exn);