From baa3e16836c3f0daf24ba47aadbdee525762d6ec Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 9 Dec 1999 23:20:18 +0000
Subject: Ajout des messages d'erreurs de Cases

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

(limited to 'kernel/inductive.mli')

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 1f1d5927fa..63e85a539c 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -106,3 +106,5 @@ val mind_extract_and_check_params :
 val mind_extract_params : int -> constr -> (name * constr) list * constr
 
 val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit
+
+val inductive_of_constructor : constructor_path -> inductive_path
-- 
cgit v1.2.3