From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Oct 2017 17:04:02 +0100
Subject: Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.
---
 kernel/kernel.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/kernel.mllib')

diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 5108744bde..59c1d5890f 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -26,6 +26,7 @@ Conv_oracle
 Environ
 Primred
 CClosure
+Retypeops
 Reduction
 Clambda
 Nativelambda
-- 
cgit v1.2.3