inductive type ident optional in mutcase

[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 edc112992121133be7071cb66939920756b6e60d..06f18080d07466aaccba41ca71b3d83599ae4678 100644 (file)
--- 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