(k', e', ens', C.MutConstruct (_,_,j,_), []) ->
reduce (k, e, ens, (List.nth pl (j-1)), s)
| (k', e', ens', C.MutConstruct (_,_,j,_), s') ->
- let (arity, r) =
+ let r =
let o,_ =
CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind
in
match o with
- C.InductiveDefinition (s,ingredients,r,_) ->
- let (_,_,arity,_) = List.nth s i in
- (arity,r)
+ C.InductiveDefinition (_,_,r,_) -> r
| _ -> raise WrongUriToInductiveDefinition
in
let ts =
let are_convertible whd ?(subst=[]) ?(metasenv=[]) =
let heuristic = ref true in
let rec aux test_equality_only context t1 t2 ugraph =
- let aux2 test_equality_only t1 t2 ugraph =
+ let rec aux2 test_equality_only t1 t2 ugraph =
(* this trivial euristic cuts down the total time of about five times ;-) *)
(* this because most of the time t1 and t2 are "sintactically" the same *)
fl1 fl2 (true,ugraph)
else
false,ugraph
- | (C.Cast _, _) | (_, C.Cast _)
+ | C.Cast (bo,_),t -> aux2 test_equality_only bo t ugraph
+ | t,C.Cast (bo,_) -> aux2 test_equality_only t bo ugraph
| (C.Implicit _, _) | (_, C.Implicit _) -> assert false
| (_,_) -> false,ugraph
end