From e01753bf730b3c4e50df0655f7940f8720b16524 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 20 Jan 2005 10:26:06 +0000 Subject: [PATCH] added cast rendering (used in check window by gTopLevel/matita) --- helm/ocaml/cic_transformations/acic2Ast.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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)) -- 2.39.2