diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-04 18:14:38 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-04 19:24:01 +0100 |
commit | c71e69a9be2094061e041d60614b090c8381f0b7 (patch) | |
tree | f2a0a62a3c53102b8c222da494ee168bd610dc8a /proofs/tacmach.mli | |
parent | f281a8a88e8fc7c41cc5680db2443d9da33b47b7 (diff) |
[api] Deprecate all legacy uses of Name.Id in core.
This is a first step towards some of the solutions proposed in #6008.
Diffstat (limited to 'proofs/tacmach.mli')
-rw-r--r-- | proofs/tacmach.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index d4e9555f3..de9f8e700 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 |