diff options
| author | filliatr | 1999-10-08 08:18:57 +0000 |
|---|---|---|
| committer | filliatr | 1999-10-08 08:18:57 +0000 |
| commit | fd28f10096f82ef133bbf10512c8bee617b6b8b3 (patch) | |
| tree | 96892fb5b66038cef8ca48b0cc3f0383e38fc9a5 /kernel/typeops.mli | |
| parent | 610caabdaac2f9ca635737839f645cc870d83975 (diff) | |
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
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 |