X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=429efbf52b4590e9e19d0e6561ef5e0bae067b26;hb=5ddacb0ce9c69c9bab984e1cd28fc65c617880a4;hp=b1e3cc73393eee4bf10e2682a278f1c0f6adcb2d;hpb=0af3592e3a85a4bb82c5c6df259cf9ab117ba0b1;p=helm.git

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index b1e3cc733..429efbf52 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: [
@@ -477,15 +481,16 @@ EXTEND
       params = LIST0 protected_binder_vars;
        SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ; 
        fields = LIST0 [ 
-         name = IDENT ; 
+         name = IDENT ;
+         params = LIST0 protected_binder_vars; (* FG: params added *)
          coercion = [ 
              SYMBOL ":" -> false,0 
            | SYMBOL ":"; SYMBOL ">" -> true,0
            | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
          ]; 
          ty = term -> 
-           let b,n = coercion in 
-           (name,ty,b,n) 
+           let b,n = coercion in
+           (name, shift_params `Forall params ty, b, n) 
        ] SEP SYMBOL ";"; SYMBOL "}" -> 
         let params =
           List.fold_right