X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=110c9e912c6b5946ddd603ae20b3a3859a3e3812;hb=0d2bfb98d8343b4e6cefdb506a813b7cb5749630;hp=837a82910bb6a53d89628c8a62d6b64b1139e429;hpb=cb11de1c61f0b61935b1c6c1832deacb49f7b5bd;p=helm.git

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 837a82910..110c9e912 100644
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -70,11 +70,6 @@ let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
 let default_associativity = Gramext.NonA
         
 let mk_rec_corec ind_kind defs loc = 
- (* In case of mutual definitions here we produce just
-    the syntax tree for the first one. The others will be
-    generated from the completely specified term just before
-    insertion in the environment. We use the flavour
-    `MutualDefinition to rememer this. *)
   let name,ty = 
     match defs with
     | (params,(N.Ident (name, None), ty),_,_) :: _ ->
@@ -88,13 +83,7 @@ let mk_rec_corec ind_kind defs loc =
     | _ -> assert false 
   in
   let body = N.Ident (name,None) in
-  let flavour =
-   if List.length defs = 1 then
-    `Definition
-   else
-    `MutualDefinition
-  in
-   (loc, N.Theorem(flavour, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular))
+   (loc, N.Theorem(`Definition, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular))
 
 let nmk_rec_corec ind_kind defs loc = 
  let loc,t = mk_rec_corec ind_kind defs loc in
@@ -411,24 +400,11 @@ EXTEND
     [ [ IDENT "definition"  ] -> `Definition
     | [ IDENT "fact"        ] -> `Fact
     | [ IDENT "lemma"       ] -> `Lemma
-    | [ IDENT "remark"      ] -> `Remark
-    | [ IDENT "theorem"     ] -> `Theorem
-    ]
-  ];
-  theorem_flavour: [
-    [ [ IDENT "definition"  ] -> `Definition
-    | [ IDENT "fact"        ] -> `Fact
-    | [ IDENT "lemma"       ] -> `Lemma
-    | [ IDENT "remark"      ] -> `Remark
+    | [ IDENT "example"     ] -> `Example
     | [ IDENT "theorem"     ] -> `Theorem
+    | [ IDENT "corollary"   ] -> `Corollary
     ]
   ];
-  inline_flavour: [
-     [ attr = theorem_flavour -> attr
-     | [ IDENT "axiom"     ]  -> `Axiom
-     | [ IDENT "variant"   ]  -> `Variant
-     ]
-  ];
   inductive_spec: [ [
     fst_name = IDENT; 
       params = LIST0 protected_binder_vars;