urimanager removed

[helm.git] / matita / components / grafite_parser / grafiteParser.ml

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 837a82910bb6a53d89628c8a62d6b64b1139e429..f0da64a51586c86ee93c4b71f64894127827fb9a 100644 (file)
--- 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;
@@ -485,9 +461,7 @@ EXTEND
         let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
         let rex = Str.regexp ("^"^ident^"$") in
         if Str.string_match rex id 0 then
-          if (try ignore (UriManager.uri_of_string uri); true
-              with UriManager.IllFormedUri _ -> false) ||
-             (try ignore (NReference.reference_of_string uri); true
+          if (try ignore (NReference.reference_of_string uri); true
               with NReference.IllFormedReference _ -> false)
           then
             L.Ident_alias (id, uri)
@@ -556,8 +530,7 @@ EXTEND
       ]
     ];
     level3_term: [
-      [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
-      | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
+      [ r = NREF -> N.NRefPattern (NReference.reference_of_string r)
       | IMPLICIT -> N.ImplicitPattern
       | id = IDENT -> N.VarPattern id
       | LPAREN; terms = LIST1 SELF; RPAREN ->