From dc2e676c9cdedea43805c21a4b3203832a985f95 Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 23 May 2001 15:13:07 +0000
Subject: amelioration des messages d'erreurs vis a vis des evars ajout
 automatique des chemins vers les sources au moment du Drop

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

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 3008c87cb4..e4464fd899 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -39,7 +39,7 @@ val judge_of_prop_contents : contents -> unsafe_judgment
 val judge_of_type : universe -> unsafe_judgment * constraints
 
 (*s Type of atomic terms. *)
-val relative : env -> 'a evar_map -> int -> unsafe_judgment
+val relative : env -> int -> unsafe_judgment
 
 val type_of_constant : env -> 'a evar_map -> constant -> types
 
@@ -85,11 +85,11 @@ val judge_of_case : env -> 'a evar_map -> case_info
     -> unsafe_judgment array -> unsafe_judgment * constraints
 
 val find_case_dep_nparams :
-  env -> 'a evar_map -> constr * constr -> inductive_family -> constr
+  env -> 'a evar_map -> constr * unsafe_judgment -> inductive_family
     -> bool * constraints
 
 val type_case_branches :
-  env -> 'a evar_map -> Inductive.inductive_type -> constr -> types
+  env -> 'a evar_map -> Inductive.inductive_type -> unsafe_judgment
     -> constr -> types array * types * constraints
 
 (*s Type of fixpoints and guard condition. *)
-- 
cgit v1.2.3