;;
let is_in_prop context subst metasenv ty =
let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
;;
let is_in_prop context subst metasenv ty =
let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
let _,context,ty = CicUtil.lookup_meta g metasenv in
try
let sort,u = typeof ~subst metasenv context ty ugraph in
let _,context,ty = CicUtil.lookup_meta g metasenv in
try
let sort,u = typeof ~subst metasenv context ty ugraph in
let order_new_goals metasenv subst open_goals ppterm =
let prop,rest = split_goals_in_prop metasenv subst open_goals in
let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in
let order_new_goals metasenv subst open_goals ppterm =
let prop,rest = split_goals_in_prop metasenv subst open_goals in
let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in