if paramodulation fails, go on with the normal auto...

[helm.git] / helm / ocaml / cic_transformations / acic2Ast.ml

diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml
index b60abf25886ea34a60658fba9f21d7926a180e5d..76be244adf4c17c09b9451a74fef1f9880119100 100644 (file)
--- a/helm/ocaml/cic_transformations/acic2Ast.ml
+++ b/helm/ocaml/cic_transformations/acic2Ast.ml
@@ -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
@@ -91,8 +83,7 @@ let ast_of_acic ids_to_inner_sorts acic =
           | `Prop | `CProp -> `Forall
         in
         idref id (Ast.Binder (binder_kind, (n, Some (aux s)), aux t))
-    | Cic.ACast (id,v,t) ->
-        idref id (Ast.Appl [idref id (Ast.Symbol ("cast", 0)); aux v; aux t])
+    | Cic.ACast (id,v,t) -> idref id (Ast.Cast (aux v, aux t))
     | Cic.ALambda (id,n,s,t) ->
         idref id (Ast.Binder (`Lambda, (n, Some (aux s)), aux t))
     | Cic.ALetIn (id,n,s,t) -> idref id (Ast.LetIn ((n, None), aux s, aux t))