From 498d22e9575ecf2515ae592a07b3f50e7648882f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 18 Jan 2015 23:49:38 +0100
Subject: Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it
 was actually calling the VM at Qed time.

---
 proofs/redexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/redexpr.ml')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 1858886731..1383d75567 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -234,7 +234,7 @@ let reduction_of_red_expr env =
 	 with Not_found ->
 	   error("unknown user-defined reduction \""^s^"\"")))
   | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
-  | CbvNative o -> (contextualize cbv_native cbv_native o, VMcast)
+  | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast)
   in
     reduction_of_red_expr
 
-- 
cgit v1.2.3