diff options
Diffstat (limited to 'proofs/tacmach.mli')
| -rw-r--r-- | proofs/tacmach.mli | 48 |
1 files changed, 24 insertions, 24 deletions
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index e0fb8fbc5..8f69358d4 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -92,46 +92,46 @@ 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 : Id.t -> 'a Proofview.Goal.t -> Globnames.global_reference + val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a + val pf_global : Id.t -> 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 + val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a - val project : 'a Proofview.Goal.t -> Evd.evar_map - val pf_env : 'a Proofview.Goal.t -> Environ.env - val pf_concl : 'a Proofview.Goal.t -> types + val project : Proofview.Goal.t -> Evd.evar_map + val pf_env : Proofview.Goal.t -> Environ.env + val pf_concl : 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 Proofview.Goal.t -> constr -> types + val pf_unsafe_type_of : Proofview.Goal.t -> constr -> 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 Proofview.Goal.t -> constr -> types + val pf_get_type_of : Proofview.Goal.t -> constr -> types (** This function entirely type-checks the term and computes its type and the implied universe constraints. *) - 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_type_of : Proofview.Goal.t -> constr -> evar_map * types + val pf_conv_x : Proofview.Goal.t -> t -> t -> bool - 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 -> (Id.t * types) list + val pf_get_new_id : Id.t -> Proofview.Goal.t -> Id.t + val pf_ids_of_hyps : Proofview.Goal.t -> Id.t list + val pf_ids_set_of_hyps : Proofview.Goal.t -> Id.Set.t + val pf_hyps_types : Proofview.Goal.t -> (Id.t * types) list - 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_get_hyp : Id.t -> Proofview.Goal.t -> named_declaration + val pf_get_hyp_typ : Id.t -> Proofview.Goal.t -> types + val pf_last_hyp : Proofview.Goal.t -> named_declaration - val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types - val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> (inductive * EInstance.t) * types + val pf_nf_concl : Proofview.Goal.t -> types + val pf_reduce_to_quantified_ind : Proofview.Goal.t -> types -> (inductive * EInstance.t) * types - val pf_hnf_constr : 'a Proofview.Goal.t -> constr -> types - val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types + val pf_hnf_constr : Proofview.Goal.t -> constr -> types + val pf_hnf_type_of : Proofview.Goal.t -> constr -> types - val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr - val pf_compute : 'a Proofview.Goal.t -> constr -> constr + val pf_whd_all : Proofview.Goal.t -> constr -> constr + val pf_compute : Proofview.Goal.t -> constr -> constr - val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr + val pf_nf_evar : Proofview.Goal.t -> constr -> constr end |