From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 25 May 2005 15:13:21 +0000 (+0000)
Subject: bugfix: "match" now works also when no type is provided for the matched term
X-Git-Tag: PRE_INDEX_1~123
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=27d7e38a25d28f5ac23582f744d6ecedfaa7d279;p=helm.git

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 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