From 2e42df1fe1e4b8276e7a4b268002e6a68d3ac619 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 6 Aug 2004 18:15:24 +0000
Subject: Amélioration message d'erreur objet de récursion de type non inductif

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

(limited to 'kernel/type_errors.mli')

diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index f9f2e04a48..ffa16968c7 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -21,7 +21,7 @@ open Environ
 type guard_error =
   (* Fixpoints *)
   | NotEnoughAbstractionInFixBody
-  | RecursionNotOnInductiveType
+  | RecursionNotOnInductiveType of constr
   | RecursionOnIllegalTerm of int * constr * int list * int list
   | NotEnoughArgumentsForFixCall of int
   (* CoFixpoints *)
-- 
cgit v1.2.3