From de7d0913ae0950fee077334879bfe1d0fc2c2813 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 25 Oct 2005 16:39:07 +0000 Subject: [PATCH] Syntax change: 1. hypotheses patterns are now separated by spaces (they used to be separated by ";") 2. terms in patterns must now be put in parentheses like tactic arguments --- helm/ocaml/cic_notation/grafiteParser.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml index 2863d5374..3ee56c218 100644 --- a/helm/ocaml/cic_notation/grafiteParser.ml +++ b/helm/ocaml/cic_notation/grafiteParser.ml @@ -67,10 +67,9 @@ EXTEND [ hyp_paths = LIST0 [ id = IDENT ; - path = OPT [SYMBOL ":" ; path = term -> path ] -> - (id,match path with Some p -> p | None -> Ast.UserInput) ] - SEP SYMBOL ";"; - goal_path = OPT [ SYMBOL <:unicode>; term = term -> term ] -> + path = OPT [SYMBOL ":" ; path = tactic_term -> path ] -> + (id,match path with Some p -> p | None -> Ast.UserInput) ]; + goal_path = OPT [ SYMBOL <:unicode>; term = tactic_term -> term ] -> let goal_path = match goal_path, hyp_paths with None, [] -> Ast.UserInput @@ -84,7 +83,7 @@ EXTEND [ res = OPT [ "in"; wanted_and_sps = - [ "match" ; wanted = term ; + [ "match" ; wanted = tactic_term ; sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] -> Some wanted,sps | sps = sequent_pattern_spec -> -- 2.39.2