| _ -> assert false
let get_types uri =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
| Cic.Constant _ -> assert false
| Cic.Variable _ -> assert false
| `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))