Make normalization of primitive projections in native_compute the sam…

…e as with other reduction machines.
gmalecha · Jun 8, 2015 · 5fab341 · 5fab341
1 parent 48a6ce6
commit 5fab341
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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 =