diff options
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 28 |
1 files changed, 14 insertions, 14 deletions
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 |