From ac8978c308f4f24f4edfbae135d99fd9dc5ea23a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 26 May 2019 00:10:29 +0200
Subject: Actually merge Discharge into Cooking.

This is the intended module for the feature provided by the inductive
discharge. This allows for a bit of code sharing and cleanup.
---
 kernel/kernel.mllib | 1 -
 1 file changed, 1 deletion(-)

(limited to 'kernel/kernel.mllib')

diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 238cbba425..59c1d5890f 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -48,5 +48,4 @@ Term_typing
 Subtyping
 Mod_typing
 Nativelibrary
-Discharge
 Safe_typing
-- 
cgit v1.2.3