diff options
| author | Pierre-Marie Pédrot | 2018-11-05 14:15:11 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-05 14:15:11 +0100 |
| commit | ebc815989728991850080da0e3033cfabecbb759 (patch) | |
| tree | 8eb9560474fabf5ee81011935747696f05f7b0b1 | |
| parent | 5202b20739d18137780b7729ee657b7eecef5c0c (diff) | |
| parent | 3f22c11c650b6ef7cc0770418255865ebdbfb1ae (diff) | |
Merge PR #8896: Expose Typing.judge_of_apply
| -rw-r--r-- | pretyping/typing.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/typing.mli b/pretyping/typing.mli index b8830ff4a2..366af0772f 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -48,6 +48,8 @@ val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map -> val judge_of_prop : unsafe_judgment val judge_of_set : unsafe_judgment +val judge_of_apply : env -> evar_map -> unsafe_judgment -> unsafe_judgment array -> + evar_map * unsafe_judgment val judge_of_abstraction : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment val judge_of_product : Environ.env -> Name.t -> |