[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.

1 files changed, 1 insertions, 2 deletions

diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 0325a00b47..3736a0f9a8 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -432,7 +432,6 @@ module Renv =
 	r
   end
 
-(* What about pattern matching ?*)
 let is_lazy prefix t =
   match kind t with
   | App (f,args) ->
@@ -448,7 +447,7 @@ let is_lazy prefix t =
 	  with Not_found -> true)
      | _ -> true
      end
-  | LetIn _ -> true
+  | LetIn _ | Case _ | Proj _ -> true
   | _ -> false
 
 let evar_value sigma ev = sigma.evars_val ev