From d72e5c154faeea1d55387bc8c039d97f63ebd1c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 3 Mar 2019 21:03:37 +0100
Subject: Change the representation of kernel case.

We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
---
 kernel/typeops.mli | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index d381e55dd6..5ea7163f72 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -92,12 +92,6 @@ val judge_of_cast :
 val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment
 val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment
 
-(** {6 Type of Cases. } *)
-val judge_of_case : env -> case_info
-  -> unsafe_judgment -> (constr,Instance.t) case_invert -> unsafe_judgment
-  -> unsafe_judgment array
-  -> unsafe_judgment
-
 (** {6 Type of global references. } *)
 
 val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
-- 
cgit v1.2.3