(function x::_ -> x | _ -> assert false) 80
(NotationPres.mpres_of_box boxml)));
*)
+ let attrs = `Generated, `Definition, pragma in
NotationPt.Theorem
- (`Definition,srec_name,
- NotationPt.Implicit `JustOne,Some res,pragma)
+ (srec_name, NotationPt.Implicit `JustOne, Some res, attrs)
;;
let ast_of_sort s =
let rec pp rels =
function
NCic.Rel i -> List.nth rels (i - 1)
- | NCic.Const _ as t ->
- NotationPt.Ident
- (status#ppterm ~metasenv:[] ~subst:[] ~context:[] t,None)
+ | NCic.Const _ as t -> NotationPt.NCic t
| NCic.Sort s -> NotationPt.Sort (fst (ast_of_sort s))
| NCic.Meta _
| NCic.Implicit _ -> assert false
| NCic.Lambda (n,s,t) ->
let n = mk_id n in
NotationPt.Binder (`Lambda, (n,Some (pp rels s)), pp (n::rels) t)
- | NCic.LetIn (n,s,ty,t) ->
+ | NCic.LetIn (n,ty,s,t) ->
let n = mk_id n in
NotationPt.LetIn ((n, Some (pp rels ty)), pp rels s, pp (n::rels) t)
| NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) ->
(function x::_ -> x | _ -> assert false)
80 (NotationPres.render (fun _ -> None)
(TermContentPres.pp_ast res)));*)
+ let attrs = `Generated, `Definition, `Projection in
NotationPt.Theorem
- (`Definition,projname,NotationPt.Implicit `JustOne,Some res,`Projection)
+ (projname, NotationPt.Implicit `JustOne, Some res, attrs)
;;
let mk_projections status (_,_,_,_,obj) =