- synced notation pretty printing with parsing syntax

[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 1e4914e7f9bbbf250830d44654710119e3df65c0..76be244adf4c17c09b9451a74fef1f9880119100 100644 (file)
--- a/helm/ocaml/cic_transformations/acic2Ast.ml
+++ b/helm/ocaml/cic_transformations/acic2Ast.ml
@@ -29,13 +29,6 @@ module Ast = CicAst
 
 let symbol_table = Hashtbl.create 1024
 
-let sort_of_string = function
-  | "Prop" -> `Prop
-  | "Set" -> `Set
-  | "Type" -> `Type
-  | "CProp" -> `CProp
-  | _ -> assert false
-
 let get_types uri =
   let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
     match o with
@@ -66,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
@@ -86,12 +79,11 @@ let ast_of_acic ids_to_inner_sorts acic =
     | Cic.AProd (id,n,s,t) ->
         let binder_kind =
           match sort_of_id id with
-          | `Set | `Type -> `Pi
+          | `Set | `Type | `Meta -> `Pi
           | `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))