From 9a913a2aa1834704908ec829d5326d214fd68e88 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 21 Mar 2000 18:16:19 +0000
Subject: Modification de type_of_case, type_case_branches, etc

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

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 90df90099b..e526d82fbf 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -40,8 +40,8 @@ val type_of_case : env -> 'a evar_map -> case_info
     -> unsafe_judgment array -> unsafe_judgment
 
 val type_case_branches :
-  env -> 'a evar_map -> constr -> constr -> constr -> constr 
-    -> constr * constr array * constr 
+  env -> 'a evar_map -> Inductive.inductive_summary -> constr -> constr
+    -> constr -> constr array * constr 
 
 val judge_of_prop_contents : contents -> unsafe_judgment
 
@@ -86,8 +86,7 @@ val make_arity_nodep :
 
 val find_case_dep_nparams :
   env -> 'a evar_map -> constr * constr ->
-    inductive * constr list ->
-      constr -> bool * (int * constr list * constr list) 
+    inductive * constr list -> constr -> bool
 
 (* The constr list is the global args list *)
 val type_inst_construct :
-- 
cgit v1.2.3