X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=06f18080d07466aaccba41ca71b3d83599ae4678;hb=5095f0f9e11e966d7872d38ab8ef408567c5984e;hp=edc112992121133be7071cb66939920756b6e60d;hpb=1fa2e1ad132b280dbf3a0fb670e4e79858a15e6d;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index edc112992..06f18080d 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -110,10 +110,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))
@@ -283,7 +296,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