From 1ed0836a7e0c8e05b0288f85e344ef5249d5d228 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 10 Nov 2017 13:23:32 +0100
Subject: Inference of inductive subtyping does not need an evar map.

---
 pretyping/inductiveops.mli | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'pretyping/inductiveops.mli')

diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 58b1ce6c3f..f6b11ee666 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -201,10 +201,5 @@ val type_of_inductive_knowing_conclusion :
 val control_only_guard : env -> types -> unit
 
 (* inference of subtyping condition for inductive types *)
-(* for debugging purposes only to be removed *)
-val infer_inductive_subtyping_arity_constructor : Environ.env * Evd.evar_map * Univ.Constraint.t ->
-(constr -> constr) ->
-types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t
-
-val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry ->
+val infer_inductive_subtyping : Environ.env -> Entries.mutual_inductive_entry ->
   Entries.mutual_inductive_entry
-- 
cgit v1.2.3