From 27d7e38a25d28f5ac23582f744d6ecedfaa7d279 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 25 May 2005 15:13:21 +0000 Subject: [PATCH] bugfix: "match" now works also when no type is provided for the matched term --- helm/ocaml/cic_disambiguation/disambiguate.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 0f169fc27..bd7b33440 100644 --- 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 -- 2.39.2