From 3f22c11c650b6ef7cc0770418255865ebdbfb1ae Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 2 Nov 2018 14:08:54 +0100
Subject: Expose Typing.judge_of_apply

This can be useful to avoid [Typing.type_of (App (f,args))] when
working with universe polymorphism.
---
 pretyping/typing.mli | 2 ++
 1 file changed, 2 insertions(+)

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 ->
-- 
cgit v1.2.3