From c53b834c50bd6933f852795d2d3dc172ac55ceb2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 26 Oct 2007 12:37:21 +0000 Subject: [PATCH] Syntax of patterns changed (and not documented yet). It is now: match p with [ _ => p | ... | _ => p ] (use lambda-abstractions for dummy arguments). Hmmm... --- components/cic_disambiguation/disambiguate.ml | 8 ++++++++ 1 file changed, 8 insertions(+) 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 = -- 2.39.2