From 55dbe8e2fa7ed2053ecd54140f6bcbdf31981e0b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 5 Oct 2006 15:40:31 +0000
Subject: Correction de deux cas où les types inductifs n'étaient pas comparés
 vis à vis de l'équivalence engendrées par les modules non génératifs (cf bug
 #1242)

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

(limited to 'kernel/closure.mli')

diff --git a/kernel/closure.mli b/kernel/closure.mli
index 88f9139e6e..2a0c1f89e3 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -179,8 +179,9 @@ val whd_stack :
 (* [unfold_reference] unfolds references in a [fconstr] *)
 val unfold_reference : clos_infos -> table_key -> fconstr option
 
-(* [mind_equiv] checks whether two mutual inductives are intentionally equal *)
-val mind_equiv : clos_infos -> mutual_inductive -> mutual_inductive -> bool
+(* [mind_equiv] checks whether two inductive types are intentionally equal *)
+val mind_equiv : env -> inductive -> inductive -> bool
+val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool
 
 (************************************************************************)
 (*i This is for lazy debug *)
-- 
cgit v1.2.3