From d44846131cf2fab2d3c45d435b84d802b1af8d43 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 15 Dec 1999 15:24:13 +0000
Subject: Nouveaux types 'constructor' et 'inductive' dans Term; les fonctions
 sur les inductifs prennent maintenant des 'inductive' en paramètres; elle
 n'ont plus besoin de faire des appels dangereux aux find_m*type qui
 centralisent la levée de raise Induc.

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

(limited to 'pretyping/pretype_errors.mli')

diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 1292ad75c4..9944f55a86 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -31,7 +31,7 @@ val error_case_not_inductive_loc :
 (* Pattern-matching errors *)
 
 val error_bad_constructor_loc : 
-  loc -> path_kind -> constructor_path -> inductive_path -> 'b
+  loc -> path_kind -> constructor -> inductive -> 'b
 
 val error_wrong_numarg_constructor_loc : 
   loc -> path_kind -> constructor_path -> int -> 'b
-- 
cgit v1.2.3