X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=fd9c2946d9476a956821248b07f0ee3deaa15042;hb=1b4d894e7349bba991823249f1716fb8f18239b7;hp=70fe2f4157621800d93c37c44f4442182d675d54;hpb=6c15dd2d7c372dc163c24e96bf56376c5bcb5a6c;p=helm.git

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 70fe2f415..fd9c2946d 100644
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -66,6 +66,12 @@ let nmk_rec_corec src ind_kind defs loc index =
  let loc,t = mk_rec_corec src ind_kind defs loc in
   G.NObj (loc,t,index)
 
+let shift_vars binder (vars, ty) bo =
+   let map var bo = N.Binder (binder, (var, ty), bo) in
+   List.fold_right map vars bo
+
+let shift_params binder params bo = 
+   List.fold_right (shift_vars binder) params bo
 (*
 let nnon_punct_of_punct = function
   | G.Skip loc -> G.NSkip loc
@@ -501,12 +507,20 @@ EXTEND
   grafite_ncommand: [ [
       IDENT "qed" ;  i = index -> G.NQed (loc,i)
     | IDENT "defined" ;  i = index -> G.NQed (loc,i) (* FG: presentational qed for definitions *)
-    | src = source; nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
+    | src = source; nflavour = ntheorem_flavour; name = IDENT;
+      params = LIST0 protected_binder_vars; SYMBOL ":"; typ = term; (* FG: params added *)
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+        let typ = shift_params `Forall params typ in
+        let body = match body with
+           | Some bo -> Some (shift_params `Lambda params bo)
+           | None    -> None
+        in
         let attrs = src, nflavour, `Regular in
 	G.NObj (loc, N.Theorem (name, typ, body, attrs),true)
-    | src = source; nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
+    | src = source; nflavour = ntheorem_flavour; name = IDENT;
+      params = LIST0 protected_binder_vars; SYMBOL <:unicode<def>> (* ≝ *); (* FG: params added *)
       body = term ->
+        let body = shift_params `Lambda params body in
         let attrs = src, nflavour, `Regular in
         G.NObj (loc, 
           N.Theorem(name, N.Implicit `JustOne, Some body, attrs),