let find_in_context name context =
let rec aux acc = function
| [] -> raise Not_found
- | (hd,_) :: tl when hd = name -> acc
+ | (hd,_) :: _ when hd = name -> acc
| _ :: tl -> aux (acc + 1) tl
in
aux 1 context
let goalty = get_goalty status goal in
let status, what = disambiguate status (ctx_of goalty) what `XTInd in
let status, ty_what = typeof status (ctx_of what) what in
- let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
+ let _status, (r,consno,lefts,rights) = analyse_indty status ty_what in
let leftno = List.length lefts in
let rightno = List.length rights in
indtyref := Some {
let goalty = get_goalty status goal in
let status,sort = typeof status (ctx_of goalty) goalty in
let status, sort = fix_sorts status sort in
- let status, sort = term_of_cic_term status sort (ctx_of goalty) in
+ let ctx = ctx_of goalty in
+ let status, sort = whd status (ctx_of sort) sort in
+ let status, sort = term_of_cic_term status sort ctx in
sortref := sort;
status)
;;
let assert_tac seqs status =
match status#stack with
| [] -> assert false
- | (g,_,_,_) :: s ->
+ | (g,_,_,_) :: _s ->
assert (List.length g = List.length seqs);
(match seqs with
[] -> id_tac