(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 =
| 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) =