From 4cc1714ac9b0944b6203c23af8c46145e7239ad3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 20 Oct 2015 14:45:31 +0200 Subject: Indexing Proofview.goals with a stage. This is not perfect though, some primitives are unsound, and some higher-order API should use polymorphic functions so as not to depend on a given level. --- proofs/tacmach.mli | 45 +++++++++++++++++++++++---------------------- 1 file changed, 23 insertions(+), 22 deletions(-) (limited to 'proofs/tacmach.mli') diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index a0e1a0157..3ed6a2eeb 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -106,36 +106,37 @@ val pr_glls : goal list sigma -> Pp.std_ppcmds (* 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 -> constr - val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a + val pf_apply : (env -> evar_map -> 'a) -> ('b, 'r) Proofview.Goal.t -> 'a + val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> constr + (** FIXME: encapsulate the level in an existential type. *) + val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a - val pf_env : 'a Proofview.Goal.t -> Environ.env - val pf_concl : [ `NF ] Proofview.Goal.t -> types + val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env + val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> 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_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types + 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 - val pf_get_new_id : identifier -> [ `NF ] Proofview.Goal.t -> identifier - val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list - val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list + val pf_get_new_id : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier + val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list + val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list - val pf_get_hyp : identifier -> [ `NF ] Proofview.Goal.t -> named_declaration - val pf_get_hyp_typ : identifier -> [ `NF ] Proofview.Goal.t -> types - val pf_last_hyp : [ `NF ] Proofview.Goal.t -> named_declaration + val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> named_declaration + val pf_get_hyp_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types + val pf_last_hyp : ([ `NF ], 'r) 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 -> pinductive * types + val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types + val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * 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 : ('a, 'r) Proofview.Goal.t -> constr -> types + val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types - val pf_whd_betadeltaiota : 'a Proofview.Goal.t -> constr -> constr - val pf_compute : 'a Proofview.Goal.t -> constr -> constr + val pf_whd_betadeltaiota : ('a, 'r) Proofview.Goal.t -> constr -> constr + val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr - val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map + val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map - val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr + val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr end -- cgit v1.2.3