X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_transformations%2Facic2Ast.ml;h=76be244adf4c17c09b9451a74fef1f9880119100;hb=cd602bc57c4ceba6188b4cac0dbf5dad8f5df7b6;hp=70036146e8240d697ab212f1f80e25c0444244cf;hpb=ff981d975589f8d21a364e7cfe875647f7483cd9;p=helm.git

diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml
index 70036146e..76be244ad 100644
--- a/helm/ocaml/cic_transformations/acic2Ast.ml
+++ b/helm/ocaml/cic_transformations/acic2Ast.ml
@@ -83,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))