Commit 1a9a65ba authored by MARCHE Claude's avatar MARCHE Claude

destruct: destructing Tcase should not happen if not at toplevel

This is because it might be non-reversible: we don't state that when a
given pattern is matched, the subject does not match the former patterns
parent 208569fe
......@@ -331,7 +331,7 @@ let destruct_fmla ~recursive (t: term) = (fun ts -> Axiom_term (t_not t1) :: ts)
ts2 @ ts3
| Tcase (t, tbs) ->
| Tcase (t, tbs) when toplevel ->
let for_branch tb =
let pat, rhs = t_open_branch tb in
let for_expansion (bds, eqs, t') =
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