From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 20 Jan 2005 10:26:06 +0000 (+0000)
Subject: added cast rendering (used in check window by gTopLevel/matita)
X-Git-Tag: V_0_1_0~119
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e01753bf730b3c4e50df0655f7940f8720b16524;p=helm.git

added cast rendering (used in check window by gTopLevel/matita)
---

diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml
index 752dd3216..b815d33bd 100644
--- a/helm/ocaml/cic_transformations/acic2Ast.ml
+++ b/helm/ocaml/cic_transformations/acic2Ast.ml
@@ -92,7 +92,8 @@ 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 (aux v)
+    | Cic.ACast (id,v,t) ->
+        idref id (Ast.Appl [idref id (Ast.Symbol ("cast", -1)); 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))