bugfix: "match" now works also when no type is provided for the matched term

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 0f169fc27ee65da0cd07920b10870fbf99ade62c..bd7b334401f68f4e4dbf8139e156697a9bc42c49 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -309,6 +309,10 @@ let domain_of_term ~context ast =
     | CicAst.Case (term, indty_ident, outtype, branches) ->
         let term_dom = aux loc context term in
         let outtype_dom = aux_option loc context outtype in
+        let get_first_constructor = function
+          | [] -> []
+          | ((head, _), _) :: _ -> [ Id head ]
+        in
         let do_branch ((head, args), term) =
           let (term_context, args_domain) =
             List.fold_left
@@ -325,7 +329,9 @@ let domain_of_term ~context ast =
           List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
         in
         branches_dom @ outtype_dom @ term_dom @
-        (match indty_ident with None -> [] | Some ident -> [ Id ident ])
+        (match indty_ident with
+         | None -> get_first_constructor branches
+         | 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