let _, sort = typeof s (ctx_of gty) gty in
match term_of_cic_term s sort (ctx_of sort) with
| _, NCic.Sort NCic.Prop -> P
let _, sort = typeof s (ctx_of gty) gty in
match term_of_cic_term s sort (ctx_of sort) with
| _, NCic.Sort NCic.Prop -> P
if has_no_alternative then (L (g,status)) else (S (g,status))in
(* TODO: cache success g *)
let pos = if has_no_alternative then Z.inject T.Nil pos else pos in
if has_no_alternative then (L (g,status)) else (S (g,status))in
(* TODO: cache success g *)
let pos = if has_no_alternative then Z.inject T.Nil pos else pos in
let news = status,size,depth in
let pos = Z.setA news newg pos in
match Z.right pos with
let news = status,size,depth in
let pos = Z.setA news newg pos in
match Z.right pos with