From b385fbbbb7868f0994d5ec00cb918cea1e8f18cf Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 4 Nov 2016 15:55:52 +0100
Subject: Use pf_get_type_of to avoid blowup in pose proof of large proof terms

---
 proofs/tacmach.mli | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index f79fa1d4b3..59f296f64e 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -108,8 +108,16 @@ module New : sig
   val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env
   val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types
 
+  (** WRONG: To be avoided at all costs, it typechecks the term entirely but
+     forgets the universe constraints necessary to retypecheck it *)
   val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types
+
+  (** This function does no type inference and expects an already well-typed term.
+      It recomputes its type in the fastest way possible (no conversion is ever involved) *)
   val pf_get_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types
+
+  (** This function entirely type-checks the term and computes its type
+      and the implied universe constraints. *)
   val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.types
   val pf_conv_x : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.constr -> bool
 
-- 
cgit v1.2.3