From 5fab341f70b05823910b9a7ead63deb7b35bf161 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Mon, 8 Jun 2015 22:36:08 +0200
Subject: Make normalization of primitive projections in native_compute the
 same as with other reduction machines.

---
 pretyping/nativenorm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/nativenorm.ml')

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index ac4e3b306..b4b6b8aab 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -271,7 +271,7 @@ and nf_atom env atom =
   | Aevar (ev,_) -> mkEvar ev
   | Aproj(p,c) ->
       let c = nf_accu env c in
-	mkProj(Projection.make p false,c)
+	mkProj(Projection.make p true,c)
   | _ -> fst (nf_atom_type env atom)
 
 and nf_atom_type env atom =
-- 
cgit v1.2.3