From 5c1768a4dcf39ffd7d58ea9448a842376e86ccf9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 5 Mar 2001 08:20:05 +0000
Subject: Re-Déplacement extended_rel_list

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1423 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/inductive.mli | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'kernel/inductive.mli')

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 4980b9196a..e1ee0a56f0 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -116,11 +116,6 @@ val build_dependent_constructor : constructor_summary -> constr
    the constructor argument of a dependent predicate in a cases branch *)
 val build_dependent_inductive : inductive_family -> constr
 
-(*s [extended_rel_vect n hyps] and [extended_rel_list n hyps]
-    generalizes [rel_vect] when local definitions may occur in parameters *)
-val extended_rel_vect : int -> rel_context -> constr array
-val extended_rel_list : int -> rel_context -> constr list
-
 (* if the arity for some inductive family [indf] associated to [(I
    params)] is [(x1:A1)...(xn:An)sort'] then [make_arity env sigma dep
    indf k] builds [(x1:A1)...(xn:An)sort] which is the arity of an
-- 
cgit v1.2.3