From fd28f10096f82ef133bbf10512c8bee617b6b8b3 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 8 Oct 1999 08:18:57 +0000
Subject: deplacements des var. ex. hors du noyau

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

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 992a3a768d..a95b54b66e 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -19,18 +19,18 @@ val j_val_only : unsafe_judgment -> constr
    constructs the typed type $t:s$, while [assumption_of_judgement env j]
    cosntructs the type type $c:t$, checking that $t$ is a sort. *)
 
-val typed_type_of_judgment : 'a unsafe_env -> unsafe_judgment -> typed_type
-val assumption_of_judgment : 'a unsafe_env -> unsafe_judgment -> typed_type
+val typed_type_of_judgment : unsafe_env -> unsafe_judgment -> typed_type
+val assumption_of_judgment : unsafe_env -> unsafe_judgment -> typed_type
 
-val relative : 'a unsafe_env -> int -> unsafe_judgment
+val relative : unsafe_env -> int -> unsafe_judgment
 
-val type_of_constant_or_existential : 'a unsafe_env -> constr -> typed_type
+val type_of_constant : unsafe_env -> constr -> typed_type
 
-val type_of_inductive : 'a unsafe_env -> constr -> typed_type
+val type_of_inductive : unsafe_env -> constr -> typed_type
 
-val type_of_constructor : 'a unsafe_env -> constr -> constr
+val type_of_constructor : unsafe_env -> constr -> constr
 
-val type_of_case : 'a unsafe_env -> unsafe_judgment -> unsafe_judgment 
+val type_of_case : unsafe_env -> unsafe_judgment -> unsafe_judgment 
   -> unsafe_judgment array -> unsafe_judgment
 
 val type_of_prop_or_set : contents -> unsafe_judgment
@@ -38,22 +38,22 @@ val type_of_prop_or_set : contents -> unsafe_judgment
 val type_of_type : universe -> unsafe_judgment * constraints
 
 val abs_rel : 
-  'a unsafe_env -> name -> typed_type -> unsafe_judgment 
+  unsafe_env -> name -> typed_type -> unsafe_judgment 
     -> unsafe_judgment * constraints
 
 val gen_rel :
-  'a unsafe_env -> name -> typed_type -> unsafe_judgment 
+  unsafe_env -> name -> typed_type -> unsafe_judgment 
     -> unsafe_judgment * constraints
 
 val cast_rel : 
-  'a unsafe_env -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment
+  unsafe_env -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment
 
 val apply_rel_list : 
-  'a unsafe_env -> bool -> unsafe_judgment list -> unsafe_judgment
+  unsafe_env -> bool -> unsafe_judgment list -> unsafe_judgment
     -> unsafe_judgment * constraints
 
-val check_fix : 'a unsafe_env -> constr -> unit
-val check_cofix : 'a unsafe_env -> constr -> unit
+val check_fix : unsafe_env -> Spset.t -> constr -> unit
+val check_cofix : unsafe_env -> Spset.t -> constr -> unit
 
-val type_fixpoint : 'a unsafe_env -> name list -> typed_type array 
+val type_fixpoint : unsafe_env -> name list -> typed_type array 
     -> unsafe_judgment array -> constraints
-- 
cgit v1.2.3