X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=ca5f1449c961826f35516c629c59f23ec7402079;hb=ae25bae855f66b7ebc9926a80dc38e622f0cff38;hp=d37819c6aa82a1f1a93dc91a473ee54c75367064;hpb=633e905cf5500b786786ede752e97386195ad463;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index d37819c6a..ca5f1449c 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -63,7 +63,9 @@ let refine metasenv context term =
         Ko
 
 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
-  snd (Environment.find item env) env num args
+  try
+    snd (Environment.find item env) env num args
+  with Not_found -> assert false
 
   (* TODO move it to Cic *)
 let find_in_environment name context =
@@ -110,10 +112,23 @@ let interpretate ~context ~env ast =
           do_branch' context args
         in
         let (indtype_uri, indtype_no) =
-          match resolve env (Id indty_ident) () with
-          | Cic.MutInd (uri, tyno, _) -> uri, tyno
-          | Cic.Implicit _ -> raise Try_again
-          | _ -> raise DisambiguateChoices.Invalid_choice
+          match indty_ident with
+          | Some indty_ident ->
+              (match resolve env (Id indty_ident) () with
+              | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
+              | Cic.Implicit _ -> raise Try_again
+              | _ -> raise DisambiguateChoices.Invalid_choice)
+          | None ->
+              let fst_constructor =
+                match branches with
+                | ((head, _), _) :: _ -> head
+                | [] -> raise DisambiguateChoices.Invalid_choice
+              in
+              (match resolve env (Id fst_constructor) () with
+              | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
+                  (indtype_uri, indtype_no)
+              | Cic.Implicit _ -> raise Try_again
+              | _ -> raise DisambiguateChoices.Invalid_choice)
         in
         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
           (List.map do_branch branches))
@@ -261,10 +276,15 @@ let domain_of_term ~context ast =
     | CicAst.AttributedTerm (_, term) -> aux loc context term
     | CicAst.Appl terms ->
         List.fold_left (fun dom term -> aux loc context term @ dom) [] terms
-    | CicAst.Binder (_, (var, typ), body) ->
+    | CicAst.Binder (kind, (var, typ), body) ->
+        let kind_dom =
+          match kind with
+          | `Exists -> [ Symbol ("exists", 0) ]
+          | _ -> []
+        in
         let type_dom = aux_option loc context typ in
         let body_dom = aux loc (var :: context) body in
-        body_dom @ type_dom
+        body_dom @ type_dom @ kind_dom
     | CicAst.Case (term, indty_ident, outtype, branches) ->
         let term_dom = aux loc context term in
         let outtype_dom = aux_option loc context outtype in
@@ -283,7 +303,8 @@ let domain_of_term ~context ast =
         let branches_dom =
           List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
         in
-        branches_dom @ outtype_dom @ term_dom @ [ Id indty_ident ]
+        branches_dom @ outtype_dom @ term_dom @
+        (match indty_ident with None -> [] | Some ident -> [ Id ident ])
     | CicAst.LetIn ((var, typ), body, where) ->
         let body_dom = aux loc context body in
         let type_dom = aux_option loc context typ in
@@ -377,13 +398,13 @@ module Make (C: Callbacks) =
        (function uri,_ ->
          MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
        ) result in
-      C.output_html (`Msg (`T "Locate query:"));
+      HelmLogger.log (`Msg (`T "Locate query:"));
       MQueryUtil.text_of_query
-       (fun s -> C.output_html ~append_NL:false (`Msg (`T s)))
+       (fun s -> HelmLogger.log ~append_NL:false (`Msg (`T s)))
        "" query; 
-      C.output_html (`Msg (`T "Result:"));
+      HelmLogger.log (`Msg (`T "Result:"));
       MQueryUtil.text_of_result
-        (fun s -> C.output_html (`Msg (`T s))) "" result;
+        (fun s -> HelmLogger.log (`Msg (`T s))) "" result;
       let uris' =
        match uris with
         | [] ->