From 359e4ffe307d7d8dd250735373fc6354a58ecff5 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 28 Oct 2006 19:35:09 +0000
Subject: Extension du polymorphisme de sorte au cas des définitions dans Type.
 (suppression au passage d'un cast dans constant_entry_of_com - ce n'est pas
 normal qu'on force le type s'il n'est pas déjà présent mais en même temps il
 semble que ce cast serve pour rafraîchir les univers algébriques...)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index aeb4d294b..43d7b33db 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -14,6 +14,7 @@ open Univ
 open Term
 open Environ
 open Entries
+open Declarations
 (*i*)
 
 (*s Typing functions (not yet tagged as safe) *)
@@ -47,6 +48,9 @@ val judge_of_variable : env -> variable -> unsafe_judgment
 (*s type of a constant *)
 val judge_of_constant : env -> constant -> unsafe_judgment
 
+val judge_of_constant_knowing_parameters :
+  env -> constant -> unsafe_judgment array -> unsafe_judgment
+
 (*s Type of application. *)
 val judge_of_apply : 
   env -> unsafe_judgment -> unsafe_judgment array
@@ -93,8 +97,9 @@ val type_fixpoint : env -> name array -> types array
 (* Kernel safe typing but applicable to partial proofs *)
 val typing : env -> constr -> unsafe_judgment
 
-(* A virer *)
-val execute : Environ.env ->
-    Term.types ->
-    Univ.Constraint.t * Univ.universes ->
-    Environ.unsafe_judgment * (Univ.Constraint.t * Univ.universes)
+val type_of_constant : env -> constant -> types
+
+val type_of_constant_type : env -> constant_type -> types
+
+val type_of_constant_knowing_parameters : 
+  env -> constant_type -> constr array -> types
-- 
cgit v1.2.3