From 54fa17c6db3db0b863cbfa6a0d4b7bf0d0641def Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 20 Feb 2004 18:00:54 +0000 Subject: [PATCH] bugfix: "in" is an IDENT, not a keyword --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index cd1de4487..efe959de8 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -203,7 +203,9 @@ EXTEND | PAREN "("; t = term; PAREN ")" -> return_term loc t ] ]; - tactic_where: [ [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ] ]; + tactic_where: [ + [ where = OPT [ IDENT "in"; ident = IDENT -> ident ] -> where ] + ]; tactic_term: [ [ t = term -> t ] ]; ident_list0: [ [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] -- 2.39.2