From 8361be1d785f8588d2d3c2a0df7a1d9239bae5a1 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 9 Oct 2018 16:45:34 +0200
Subject: Remove a few circumvolutions around parameters of inductive entries

---
 kernel/typeops.mli | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 57acdfe4b5..9312b993df 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -12,7 +12,6 @@ open Names
 open Constr
 open Univ
 open Environ
-open Entries
 
 (** {6 Typing functions (not yet tagged as safe) }
 
@@ -27,8 +26,8 @@ val infer      : env -> constr       -> unsafe_judgment
 val infer_v    : env -> constr array -> unsafe_judgment array
 val infer_type : env -> types        -> unsafe_type_judgment
 
-val infer_local_decls :
-  env -> (Id.t * local_entry) list -> (env * Constr.rel_context)
+val check_context :
+  env -> Constr.rel_context -> env
 
 (** {6 Basic operations of the typing machine. } *)
 
-- 
cgit v1.2.3