let proof,goal = status in
let curi, metasenv, pbo, pty, attrs = proof in
let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in
let proof,goal = status in
let curi, metasenv, pbo, pty, attrs = proof in
let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in
| C.Appl [C.MutInd (uri, 0, []); ty; t1; t2]
when LibraryObjects.is_eq_URI uri ->
let ind_uri =
| C.Appl [C.MutInd (uri, 0, []); ty; t1; t2]
when LibraryObjects.is_eq_URI uri ->
let ind_uri =
- if_right_to_left dir2
- LibraryObjects.eq_ind_URI LibraryObjects.eq_ind_r_URI
+ match gsort with
+ C.Sort C.Prop ->
+ if_right_to_left dir2
+ LibraryObjects.eq_ind_URI LibraryObjects.eq_ind_r_URI
+ | C.Sort C.Set ->
+ if_right_to_left dir2
+ LibraryObjects.eq_rec_URI LibraryObjects.eq_rec_r_URI
+ | _ ->
+ if_right_to_left dir2
+ LibraryObjects.eq_rect_URI LibraryObjects.eq_rect_r_URI