X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;fp=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=112970d3e38f5f3aeb4219bc78752f390cd298cc;hb=53b8e2af661ad4165aa0b1deccd0a7522d96ce2e;hp=ba58eda87caff6aceebf2f18661d65af23066efb;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index ba58eda87..112970d3e 100644
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -59,21 +59,8 @@ let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
 let default_associativity = Gramext.NonA
         
 let mk_rec_corec ind_kind defs loc = 
-  let name,ty = 
-    match defs with
-    | (params,(N.Ident (name, None), ty),_,_) :: _ ->
-        let ty = match ty with Some ty -> ty | None -> N.Implicit `JustOne in
-        let ty =
-         List.fold_right
-          (fun var ty -> N.Binder (`Pi,var,ty)
-          ) params ty
-        in
-         name,ty
-    | _ -> assert false 
-  in
-  let body = N.Ident (name,None) in
-   let attrs = `Provided, `Definition, `Regular in 
-   (loc, N.Theorem(name, ty, Some (N.LetRec (ind_kind, defs, body)), attrs))
+ let attrs = `Provided, `Definition, `Regular in
+  (loc, N.LetRec (ind_kind, defs, attrs))
 
 let nmk_rec_corec ind_kind defs loc index = 
  let loc,t = mk_rec_corec ind_kind defs loc in
@@ -255,6 +242,7 @@ EXTEND
    | IDENT "width"
    | IDENT "size"
    | IDENT "nohyps"
+(*   | IDENT "timeout" *)
    ]
 ];
   auto_params: [