match obj with
| NotationPt.Inductive (_,(name,_,_,_)::_)
| NotationPt.Record (_,name,_,_) -> name ^ ".ind"
match obj with
| NotationPt.Inductive (_,(name,_,_,_)::_)
| NotationPt.Record (_,name,_,_) -> name ^ ".ind"
- | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
+ | NotationPt.Theorem (name,_,_,_) -> name ^ ".con"