[native_compute] Delay computations with toplevel match

This is an easy improvement on examples like:

Fixpoint zero (n : nat) :=
  match n with
  | O => O
  | S p => zero p + zero p
  end.

Definition foo := if true then zero 100 else 0.

Eval native_compute in if true then 0 else foo.

I didn't add a test case, because our current testing infrastructure is too
fragile for that.

0 files changed, 0 insertions, 0 deletions