CicUnification.fo_unif metasenv [] body_type ty ugraph
in
if metasenv <> [] then
- command_error
- "metasenv not empty while giving a definition with body";
+ command_error (
+ "metasenv not empty while giving a definition with body: " ^
+ CicMetaSubst.ppmetasenv metasenv []) ;
let body = CicMetaSubst.apply_subst subst body in
let ty = CicMetaSubst.apply_subst subst ty in
let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in