]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/grafite/grafiteAst.ml
1. metadata are no longer stored in .moo files.
[helm.git] / helm / ocaml / grafite / grafiteAst.ml
index a7b0f3eea365541a15647a4e1919453702abfe13..3d176fbe5190d721f0728c85f7b7c3b28ddbbec0 100644 (file)
@@ -112,14 +112,6 @@ type alias_spec =
   | Symbol_alias of string * int * string (* name, instance no, description *)
   | Number_alias of int * string          (* instance no, description *)
 
-type metadata =
-  | Dependency of string  (* baseuri without trailing slash *)
-  | Baseuri of string 
-
-let compare_metadata = Pervasives.compare
-
-let eq_metadata = (=)
-
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
 let magic = 4
@@ -145,8 +137,6 @@ type ('term,'obj) command =
         CicNotationPt.cic_appl_pattern
       (* description (i.e. id), symbol, arg pattern, appl pattern *)
 
-  | Metadata of loc * metadata
-
     (* DEBUGGING *)
   | Dump of loc (* dump grammar on stdout *)
     (* DEBUGGING *)
@@ -155,26 +145,6 @@ type ('term,'obj) command =
 (* composed magic: term + command magics. No need to change this value *)
 let magic = magic + 10000 * CicNotationPt.magic
 
-let reash_cmd_uris =
-  let reash_uri uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in
-  function
-  | Default (loc, name, uris) ->
-      let uris = List.map reash_uri uris in
-      Default (loc, name, uris)
-  | Interpretation (loc, dsc, args, cic_appl_pattern) ->
-      let rec aux =
-        function
-        | CicNotationPt.UriPattern uri ->
-            CicNotationPt.UriPattern (reash_uri uri)
-        | CicNotationPt.ApplPattern args ->
-            CicNotationPt.ApplPattern (List.map aux args)
-        | CicNotationPt.VarPattern _
-        | CicNotationPt.ImplicitPattern as pat -> pat
-      in
-      let appl_pattern = aux cic_appl_pattern in
-      Interpretation (loc, dsc, args, appl_pattern)
-  | cmd -> cmd
-
 type ('term, 'lazy_term, 'reduction, 'ident) tactical =
   | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
   | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactical