From: Stefano Zacchiroli Date: Tue, 15 Nov 2005 13:18:14 +0000 (+0000) Subject: removed grammar rule which used to enable things linke "theorem a." X-Git-Tag: V_0_7_2_3~78 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5a1134e3fcc52d74a774595abc6a481c72ae2bb5;p=helm.git removed grammar rule which used to enable things linke "theorem a." --- diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml index f8840cd77..cf2f7b1fc 100644 --- a/helm/ocaml/cic_notation/grafiteParser.ml +++ b/helm/ocaml/cic_notation/grafiteParser.ml @@ -446,10 +446,10 @@ EXTEND | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> GrafiteAst.Obj (loc,GrafiteAst.Theorem (flavour, name, typ, body)) - | flavour = theorem_flavour; name = IDENT; - body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode> (* ≝ *); + body = term -> GrafiteAst.Obj (loc, - GrafiteAst.Theorem (flavour, name, Ast.Implicit, body)) + GrafiteAst.Theorem (flavour, name, Ast.Implicit, Some body)) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = CicNotationParser.let_defs -> let name,ty = @@ -462,10 +462,10 @@ EXTEND let body = Ast.Ident (name,None) in GrafiteAst.Obj (loc,GrafiteAst.Theorem(`Definition, name, ty, Some (Ast.LetRec (ind_kind, defs, body)))) - | [ IDENT "inductive" ]; spec = inductive_spec -> + | IDENT "inductive"; spec = inductive_spec -> let (params, ind_types) = spec in GrafiteAst.Obj (loc,GrafiteAst.Inductive (params, ind_types)) - | [ IDENT "coinductive" ]; spec = inductive_spec -> + | IDENT "coinductive"; spec = inductive_spec -> let (params, ind_types) = spec in let ind_types = (* set inductive flags to false (coinductive) *) List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) @@ -490,7 +490,7 @@ EXTEND | IDENT "interpretation"; id = QSTRING; (symbol, args, l3) = interpretation -> GrafiteAst.Interpretation (loc, id, (symbol, args), l3) - | IDENT "metadata"; [IDENT "dependency" | IDENT "baseuri" ] ; URI -> + | IDENT "metadata"; [ IDENT "dependency" | IDENT "baseuri" ] ; URI -> (** metadata commands lives only in .moo, where they are in marshalled * form *) raise (CicNotationParser.Parse_error (loc, "metadata not allowed here"))