From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- proofs/tacmach.mli | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'proofs/tacmach.mli') diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index f7fc6b54..a0e1a015 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -41,7 +41,8 @@ val pf_nth_hyp_id : goal sigma -> int -> Id.t val pf_last_hyp : goal sigma -> named_declaration val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr -val pf_type_of : goal sigma -> constr -> types +val pf_unsafe_type_of : goal sigma -> constr -> types +val pf_type_of : goal sigma -> constr -> evar_map * types val pf_hnf_type_of : goal sigma -> constr -> types val pf_get_hyp : goal sigma -> Id.t -> named_declaration @@ -112,7 +113,8 @@ module New : sig val pf_env : 'a Proofview.Goal.t -> Environ.env val pf_concl : [ `NF ] Proofview.Goal.t -> types - val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types + val pf_unsafe_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types + val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> evar_map * Term.types val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool val pf_get_new_id : identifier -> [ `NF ] Proofview.Goal.t -> identifier -- cgit v1.2.3