From d4a5f73930368705b8ce07c11ecff94e04465acb Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 23 Jan 2004 17:41:17 +0000 Subject: [PATCH] handle Cic.Anonymous --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index d60e56378..0ac8ab380 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -86,7 +86,8 @@ EXTEND term: [ "arrow" RIGHTA [ t1 = term; SYMBOL <:unicode>; t2 = term -> - return_term loc (CicTextualParser2Ast.Binder (`Pi, Cic.Anonymous, Some t1, t2)) + return_term loc + (CicTextualParser2Ast.Binder (`Pi, Cic.Anonymous, Some t1, t2)) ] | "eq" LEFTA [ t1 = term; SYMBOL "="; t2 = term -> @@ -97,13 +98,18 @@ EXTEND | "inv" NONA [ (* nothing here by default *) ] | "simple" NONA [ - (* TODO handle "_" *) b = binder; vars = LIST1 IDENT SEP SYMBOL ","; typ = OPT [ SYMBOL ":"; t = term -> t ]; SYMBOL "."; body = term -> let binder = List.fold_right - (fun var body -> CicTextualParser2Ast.Binder (b, Cic.Name var, typ, body)) + (fun var body -> + let name = + match var with + | "_" -> Cic.Anonymous + | var -> Cic.Name var + in + CicTextualParser2Ast.Binder (b, name, typ, body)) vars body in return_term loc binder @@ -115,7 +121,6 @@ EXTEND | LPAREN "("; head = term; args = LIST1 term; RPAREN ")" -> return_term loc (CicTextualParser2Ast.Appl (head :: args)) | i = NUM -> return_term loc (CicTextualParser2Ast.Num (i, 0)) -(* | i = NUM -> return_term loc (CicTextualParser2Ast.Num (i, Random.int max_int)) *) | m = META; substs = [ LPAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; RPAREN "]" -> -- 2.39.2