let d =
try
Some (RS.from_env_for_unwind ~unwind (List.nth e (n-m-1)))
- with _ -> None
+ with Failure _ -> None
in
(match d with
Some t' ->
in
(match decofix (reduce (k,e,ens,term,[])) with
(k', e', ens', C.MutConstruct (_,_,j,_), []) ->
- reduce (k, e, ens, (List.nth pl (j-1)), [])
+ reduce (k, e, ens, (List.nth pl (j-1)), s)
| (k', e', ens', C.MutConstruct (_,_,j,_), s') ->
let (arity, r) =
let o,_ =
try
Some (RS.from_stack (List.nth s recindex))
with
- _ -> None
+ Failure _ -> None
in
(match recparam with
Some recparam ->
end
in
debug t1 [t2] "PREWHD";
- let t1' = whd ~delta:true ~subst context t1 in
- let t2' = whd ~delta:true ~subst context t2 in
+ let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in
+ let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
debug t1' [t2'] "POSTWHD";
aux2 test_equality_only t1' t2' ugraph
in