let module Ast = CicAst in
let idref id t = Ast.AttributedTerm (`IdRef id, t) in
let rec aux = function
- | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, []))
+ | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, None))
| Cic.AVar (id,uri,subst) ->
register_uri id (UriManager.string_of_uri uri);
idref id
| Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, astcontext_of_ciccontext l))
| Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
| Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
- | Cic.ASort (id,Cic.Type) -> idref id (Ast.Sort `Type)
+ | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type) (* TASSI *)
| Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
| Cic.AImplicit _ -> assert false
| Cic.AProd (id,n,s,t) ->
| _ -> assert false)
with Not_found -> assert false
in
- idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, [])))
+ idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None)))
| Cic.ACoFix (id, no, funs) ->
let defs =
List.map
| _ -> assert false)
with Not_found -> assert false
in
- idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, [])))
+ idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, None)))
and astsubst_of_cicsubst subst =
- List.map (fun (uri, annterm) -> (UriManager.name_of_uri uri, aux annterm))
- subst
+ Some
+ (List.map (fun (uri, annterm) ->
+ (UriManager.name_of_uri uri, aux annterm))
+ subst)
and astcontext_of_ciccontext context =
List.map