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
---
 kernel/typeops.mli | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 55191e284f..a7aec8cde5 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -27,12 +27,11 @@ val assumption_of_judgment :
 
 val relative : env -> int -> unsafe_judgment
 
-val type_of_constant : env -> 'a evar_map -> constr -> typed_type
+val type_of_constant : env -> 'a evar_map -> constant -> typed_type
 
-val type_of_inductive : env -> 'a evar_map -> constr -> typed_type
+val type_of_inductive : env -> 'a evar_map -> inductive -> typed_type
 
-val type_of_constructor :
-  env -> 'a evar_map -> (constructor_path * constr array) -> constr
+val type_of_constructor : env -> 'a evar_map -> constructor -> constr
 
 val type_of_existential : env -> 'a evar_map -> constr -> constr
 
@@ -89,10 +88,12 @@ val make_arity_nodep :
 
 val find_case_dep_nparams :
   env -> 'a evar_map -> constr * constr ->
-    constr * constr list ->
+    inductive * constr list ->
       constr -> bool * (int * constr list * constr list) 
 
-val type_inst_construct : env -> 'a evar_map -> int -> constr -> constr 
+(* The constr list is the global args list *)
+val type_inst_construct :
+  env -> 'a evar_map -> int -> inductive * constr list -> constr 
 
 val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool
 
-- 
cgit v1.2.3