where_dom @ defs_dom
| CicNotationPt.Ident (name, subst) ->
(try
- let index = find_in_context name context in
+ (* the next line can raise Not_found *)
+ ignore(find_in_context name context);
if subst <> None then
CicNotationPt.fail loc "Explicit substitutions not allowed here"
else