* src/opslexp.ml (lexp_defs_subst): Fix definition

* src/lparse.ml (elab_check_sort): Improve error message.
(elab_check_def): Use better location in error message.
(build_var): Remove.
(_lexp_p_infer): Improve error message.