From c540f6dea7b1a525a4b927a37ffba64d11a8b02a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 29 Nov 2000 11:29:48 +0000
Subject: Déplacement du message d'erreur de gen_rel vers l'appelant pour le
 prétypage

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

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 9f2bde9b88..d515948222 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -55,7 +55,7 @@ val abs_rel :
 
 (*s Type of a product. *)
 val gen_rel :
-  env -> 'a evar_map -> name -> unsafe_type_judgment -> unsafe_judgment 
+  env -> 'a evar_map -> name -> unsafe_type_judgment -> unsafe_type_judgment 
     -> unsafe_judgment * constraints
 
 val sort_of_product : sorts -> sorts -> universes -> sorts * constraints
-- 
cgit v1.2.3