diff options
Diffstat (limited to 'proofs/tacmach.mli')
| -rw-r--r-- | proofs/tacmach.mli | 34 |
1 files changed, 10 insertions, 24 deletions
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 7c96bd93bc..1ca15d9ae1 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -134,31 +134,17 @@ val pr_glls : goal list sigma -> Pp.std_ppcmds (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig - open Goal open Proofview - val pf_apply : (env -> evar_map -> 'a) -> 'a glist tactic - val pf_global_sensitive : identifier -> constr sensitive - val pf_global : identifier -> constr glist tactic - val of_old : (Proof_type.goal Evd.sigma -> 'a) -> 'a glist tactic - - val pf_get_new_id : identifier -> identifier glist tactic - val pf_ids_of_hyps_sensitive : identifier list sensitive - val pf_ids_of_hyps : identifier list glist tactic - val pf_hyps_types : (identifier * types) list glist tactic - - val pf_get_hyp_sensitive : identifier -> named_declaration sensitive - val pf_get_hyp : identifier -> named_declaration glist tactic - val pf_get_hyp_typ_sensitive : identifier -> types sensitive - val pf_get_hyp_typ : identifier -> types glist tactic - val pf_last_hyp : named_declaration glist tactic -end - - - - - - - + val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a + val pf_global : identifier -> Proofview.Goal.t -> constr + val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a + val pf_get_new_id : identifier -> Proofview.Goal.t -> identifier + val pf_ids_of_hyps : Proofview.Goal.t -> identifier list + val pf_hyps_types : Proofview.Goal.t -> (identifier * types) list + val pf_get_hyp : identifier -> Proofview.Goal.t -> named_declaration + val pf_get_hyp_typ : identifier -> Proofview.Goal.t -> types + val pf_last_hyp : Proofview.Goal.t -> named_declaration +end |