From c71e69a9be2094061e041d60614b090c8381f0b7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 4 Nov 2017 18:14:38 +0100 Subject: [api] Deprecate all legacy uses of Name.Id in core. This is a first step towards some of the solutions proposed in #6008. --- proofs/tacmach.mli | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'proofs') diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index d4e9555f34..de9f8e700b 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -97,7 +97,7 @@ val pr_glls : goal list sigma -> Pp.t (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a - val pf_global : identifier -> 'a Proofview.Goal.t -> Globnames.global_reference + val pf_global : Id.t -> 'a Proofview.Goal.t -> Globnames.global_reference (** FIXME: encapsulate the level in an existential type. *) val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a @@ -118,13 +118,13 @@ module New : sig val pf_type_of : 'a Proofview.Goal.t -> constr -> evar_map * types val pf_conv_x : 'a Proofview.Goal.t -> t -> t -> bool - val pf_get_new_id : identifier -> 'a Proofview.Goal.t -> identifier - val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list + val pf_get_new_id : Id.t -> 'a Proofview.Goal.t -> Id.t + val pf_ids_of_hyps : 'a Proofview.Goal.t -> Id.t list val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Id.Set.t - val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list + val pf_hyps_types : 'a Proofview.Goal.t -> (Id.t * types) list - val pf_get_hyp : identifier -> 'a Proofview.Goal.t -> named_declaration - val pf_get_hyp_typ : identifier -> 'a Proofview.Goal.t -> types + val pf_get_hyp : Id.t -> 'a Proofview.Goal.t -> named_declaration + val pf_get_hyp_typ : Id.t -> 'a Proofview.Goal.t -> types val pf_last_hyp : 'a Proofview.Goal.t -> named_declaration val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types -- cgit v1.2.3