From 15212e44902f25536f6e2de4bec4cedcd9a9804d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 18 Mar 2021 15:10:29 +0100 Subject: [PATCH] grafite parser updated + syntax for parameters added to constructors as it was done with definitions some time ago --- matita/components/grafite_parser/grafiteParser.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index b1e3cc733..929e68e3c 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -94,7 +94,11 @@ let mk_parser statement lstatus = (* {{{ parser initialization *) EXTEND GLOBAL: term statement; - constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; + constructor: [ + [ name = IDENT; params = LIST0 protected_binder_vars; SYMBOL ":"; typ = term -> (* FG: params added *) + (name, shift_params `Forall params typ) + ] + ]; tactic_term: [ [ t = term LEVEL "90" -> t ] ]; ident_list1: [ [ LPAREN; idents = LIST1 IDENT; RPAREN -> idents ] ]; nreduction_kind: [ -- 2.39.2