in
let name =
match obj with
- | NotationPt.Inductive (_,(name,_,_,_)::_)
- | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
- | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
+ | NotationPt.Inductive (_,(name,_,_,_)::_,_)
+ | NotationPt.Record (_,name,_,_,_) -> name ^ ".ind"
+ | NotationPt.Theorem (name,_,_,_) -> name ^ ".con"
+ | NotationPt.LetRec (_,(_,(NotationPt.Ident (name, None),_),_,_)::_,_) -> name ^ ".con"
+ | NotationPt.LetRec _
| NotationPt.Inductive _ -> assert false
in
NUri.uri_of_string (baseuri ^ "/" ^ name)