Commit 666aeb68 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

fixed eliminate_inductive with let-in

parent bbafe47e
......@@ -27,7 +27,11 @@ let exi vl (_,f) =
| Tapp (_,tl) ->
let marry acc v t = t_and_simp acc (t_equ v t) in
List.fold_left2 marry t_true vl tl
| _ -> assert false
| Tlet (t, tb) ->
let v, f = t_open_bound tb in
t_let_close v t (descend f)
| _ ->
assert false (* ensured by Decl.create_ind_decl *)
in
descend f
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment