* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
(* converts annotated terms into cic terms (forgetting ids and names) *)
let rec deannotate_term =
let module C = Cic in
in
C.Meta (n, l')
| C.ASort (_,s) -> C.Sort s
- | C.AImplicit _ -> C.Implicit
+ | C.AImplicit (_, annotation) -> C.Implicit annotation
| C.ACast (_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty)
| C.AProd (_,name,so,ta) ->
C.Prod (name, deannotate_term so, deannotate_term ta)
let deannotate_obj =
let module C = Cic in
function
- C.AConstant (_, _, id, bo, ty, params) ->
+ C.AConstant (_, _, id, bo, ty, params, attrs) ->
C.Constant (id,
(match bo with None -> None | Some bo -> Some (deannotate_term bo)),
- deannotate_term ty, params)
- | C.AVariable (_, name, bo, ty, params) ->
+ deannotate_term ty, params, attrs)
+ | C.AVariable (_, name, bo, ty, params, attrs) ->
C.Variable (name,
(match bo with None -> None | Some bo -> Some (deannotate_term bo)),
- deannotate_term ty, params)
- | C.ACurrentProof (_, _, name, conjs, bo, ty, params) ->
+ deannotate_term ty, params, attrs)
+ | C.ACurrentProof (_, _, name, conjs, bo, ty, params, attrs) ->
C.CurrentProof (
name,
List.map
List.map
(function
_,Some (n,(C.ADef at)) ->
- Some (n,(C.Def (deannotate_term at)))
+ Some (n,(C.Def ((deannotate_term at),None)))
| _,Some (n,(C.ADecl at)) ->
Some (n,(C.Decl (deannotate_term at)))
| _,None -> None
in
(id,context,deannotate_term con)
) conjs,
- deannotate_term bo,deannotate_term ty,params
+ deannotate_term bo,deannotate_term ty, params, attrs
)
- | C.AInductiveDefinition (_, tys, params, parno) ->
+ | C.AInductiveDefinition (_, tys, params, parno, attrs) ->
C.InductiveDefinition (List.map deannotate_inductiveType tys,
- params, parno)
+ params, parno, attrs)
;;