From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 18 Mar 2021 14:10:29 +0000 (+0100)
Subject: grafite parser updated
X-Git-Tag: make_still_working~151
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=15212e44902f25536f6e2de4bec4cedcd9a9804d

grafite parser updated

+ syntax for parameters added to constructors
  as it was done with definitions some time ago
---

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: [