From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 26 Oct 2007 12:37:21 +0000 (+0000)
Subject: Syntax of patterns changed (and not documented yet).
X-Git-Tag: 0.4.95@7852~92
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=c53b834c50bd6933f852795d2d3dc172ac55ceb2

Syntax of patterns changed (and not documented yet).
It is now:
 match p with [ _ => p | ... | _ => p ]
(use lambda-abstractions for dummy arguments). Hmmm...
---

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index 1fea41921..dbdb1530f 100644
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/components/cic_disambiguation/disambiguate.ml
@@ -247,6 +247,14 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                 raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
         in
         let branches =
+         if create_dummy_ids then
+          List.map
+           (function
+               Ast.Wildcard,term -> ("wildcard",None,[]), term
+             | Ast.Pattern _,_ ->
+                raise (Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
+           ) branches
+         else
          match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with
             Cic.InductiveDefinition (il,_,leftsno,_) ->
              let _,_,_,cl =