diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-06-08 22:36:08 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-06-08 22:36:08 +0200 |
| commit | 5fab341f70b05823910b9a7ead63deb7b35bf161 (patch) | |
| tree | 4a6551ff53416ab4682de0717357edf2d55fec0c /pretyping/nativenorm.ml | |
| parent | 48a6ce6e7cbdc2a03767c61696425cd5d5827f4f (diff) | |
Make normalization of primitive projections in native_compute the same as with other reduction machines.
Diffstat (limited to 'pretyping/nativenorm.ml')
| -rw-r--r-- | pretyping/nativenorm.ml | 2 |
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 = |