]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/acic2Ast.ml
Changed type of ids_to_inner_sort table used in transformation.
[helm.git] / helm / ocaml / cic_transformations / acic2Ast.ml
index b60abf25886ea34a60658fba9f21d7926a180e5d..70036146e8240d697ab212f1f80e25c0444244cf 100644 (file)
@@ -29,14 +29,6 @@ module Ast = CicAst
 
 let symbol_table = Hashtbl.create 1024
 
-let sort_of_string = function
-  | "Prop" -> `Prop
-  | "Set" -> `Set
-  | "Type" -> `Type
-  | "CProp" -> `CProp
-  | "?" -> `Meta
-  | _ -> assert false
-
 let get_types uri =
   let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
     match o with
@@ -67,7 +59,7 @@ let ast_of_acic ids_to_inner_sorts acic =
   let register_uri id uri = Hashtbl.add ids_to_uris id uri in
   let sort_of_id id =
     try
-      sort_of_string (Hashtbl.find ids_to_inner_sorts id)
+      Hashtbl.find ids_to_inner_sorts id
     with Not_found -> assert false
   in
   let idref id t = Ast.AttributedTerm (`IdRef id, t) in