diff options
| author | aspiwack | 2013-11-02 15:38:32 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:38:32 +0000 |
| commit | 00d30f5330f4f1dd487d5754a0fb855a784efbf0 (patch) | |
| tree | def0f4e640f71192748a2e964b92b9418970a98d /proofs/tacmach.mli | |
| parent | ea879916e09cd19287c831152d7ae2a84c61f4b0 (diff) | |
Tachmach.New is now in Proofview.Goal.enter style.
As a result the use of the glist-style interface for manipulating goals has almost been removed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17001 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |