aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/nativenorm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/nativenorm.ml')
-rw-r--r--pretyping/nativenorm.ml2
1 files changed, 1 insertions, 1 deletions
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 =