params @
[p_name] @
k_names @
- List.map (fun _ -> CicNotationPt.Implicit)
+ List.map (fun _ -> CicNotationPt.Implicit `JustOne)
(List.tl args) @
[mk_appl (name::abs)])))
| _ -> mk_id name,None
(function x::_ -> x | _ -> assert false) 80
(CicNotationPres.mpres_of_box boxml)));
*)
- CicNotationPt.Theorem (`Definition,srec_name,CicNotationPt.Implicit,Some res)
+ CicNotationPt.Theorem
+ (`Definition,srec_name,CicNotationPt.Implicit `JustOne,Some res)
;;
let ast_of_sort s =
(function x::_ -> x | _ -> assert false)
80 (CicNotationPres.render (fun _ -> None)
(TermContentPres.pp_ast res)));*)
- CicNotationPt.Theorem (`Definition,projname,CicNotationPt.Implicit,Some res)
+ CicNotationPt.Theorem
+ (`Definition,projname,CicNotationPt.Implicit `JustOne,Some res)
;;
let mk_projections (_,_,_,_,obj) =