From fb45e9d4b640a39b8792b1fe6381d3e12fa6c883 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 18 Nov 2011 15:00:17 +0000 Subject: [PATCH] /by {}/ ==> /by/ --- matita/components/grafite_parser/grafiteParser.ml | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 37569bea6..480c2de48 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -102,9 +102,6 @@ EXTEND constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; tactic_term: [ [ t = term LEVEL "90" -> t ] ]; ident_list1: [ [ LPAREN; idents = LIST1 IDENT; RPAREN -> idents ] ]; - tactic_term_list1: [ - [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ] - ]; nreduction_kind: [ [ IDENT "normalize" ; delta = OPT [ IDENT "nodelta" -> () ] -> let delta = match delta with None -> true | _ -> false in @@ -196,9 +193,6 @@ EXTEND | Some (`Univ univ) -> G.NTactic(loc, [G.NAuto(loc,(Some univ,["depth",depth]@params))]) - | Some `EmptyUniv -> - G.NTactic(loc, - [G.NAuto(loc,(Some [],["depth",depth]@params))]) | Some `Trace -> G.NMacro(loc, G.NAutoInteractive (loc, (None,["depth",depth]@params)))) @@ -272,8 +266,7 @@ EXTEND | i = auto_fixed_param ; SYMBOL "="; v = [ v = int -> string_of_int v | v = IDENT -> v ] -> i,v ]; just = OPT [ IDENT "by"; by = - [ univ = tactic_term_list1 -> `Univ univ - | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv + [ univ = LIST0 tactic_term SEP SYMBOL "," -> `Univ univ | SYMBOL "_" -> `Trace ] -> by ] -> just,params ] ]; -- 2.39.2