From 6c28c8f38c6f47cc772d42e5cc54398785d63bc0 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 23 Nov 1999 17:39:25 +0000
Subject: modules Indrec, Tacentries, Hiddentac

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

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index cb7f97ec57..45db129741 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -1,4 +1,3 @@
-
 (* $Id$ *)
 
 (*i*)
@@ -66,3 +65,22 @@ val check_cofix : unsafe_env -> 'a evar_map -> Spset.t -> constr -> unit
 
 val type_fixpoint : unsafe_env -> 'a evar_map -> name list -> typed_type array 
     -> unsafe_judgment array -> constraints
+
+val type_one_branch_dep : unsafe_env -> 'a evar_map -> 
+  int * constr list * constr -> constr -> constr -> constr 
+
+val type_one_branch_nodep : unsafe_env -> 'a evar_map -> 
+  int * constr list * constr -> constr -> constr 
+
+val make_arity_dep : 
+  unsafe_env -> 'a evar_map -> constr -> constr -> constr -> constr 
+
+val make_arity_nodep : 
+  unsafe_env -> 'a evar_map -> constr -> constr -> constr 
+
+val find_case_dep_nparams :
+  unsafe_env -> 'a evar_map -> constr * constr ->
+    constr * constr list ->
+      constr -> bool * (int * constr list * constr list) 
+
+val type_inst_construct : unsafe_env -> 'a evar_map -> int -> constr -> constr 
-- 
cgit v1.2.3