From a51cce369b9c634a93120092d4c7685a242d55b1 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Sat, 4 Jul 2015 14:22:08 +0200
Subject: Fix handling of primitive projections in VM.

I'm pushing this patch now because the previous treatment of such projections
in the VM was already unsound. It should however be carefully reviewed.
---
 pretyping/pretyping.mllib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/pretyping.mllib')

diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 25d17c7c9..a644e3d10 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -3,8 +3,8 @@ Termops
 Namegen
 Evd
 Reductionops
-Vnorm
 Inductiveops
+Vnorm
 Arguments_renaming
 Nativenorm
 Retyping
-- 
cgit v1.2.3