diff options
Diffstat (limited to 'plugins/ssr/ssripats.mli')
-rw-r--r-- | plugins/ssr/ssripats.mli | 108 |
1 files changed, 37 insertions, 71 deletions
diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli index 6c36e67e8..d80d14c85 100644 --- a/plugins/ssr/ssripats.mli +++ b/plugins/ssr/ssripats.mli @@ -6,77 +6,43 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* This file implements: + - the [=>] tactical + - the [:] pseudo-tactical for move, case, elim and abstract -open Ssrmatching_plugin -open Ssrast -open Ssrcommon - -type block_names = (int * EConstr.types array) option - -(* For case/elim with eq generation: args are elim_tac introeq_tac ipats - * elim E : "=> ipats" where E give rise to introeq_tac *) -val tclEQINTROS : - ?ind:block_names ref -> - ?ist:ist -> - v82tac -> - v82tac -> ssripats -> v82tac -(* special case with no eq and tactic taking ist *) -val tclINTROS : - ist -> - (ist -> v82tac) -> - ssripats -> v82tac - -(* move=> ipats *) -val introstac : ?ist:ist -> ssripats -> v82tac - -val elim_intro_tac : - Ssrast.ssripats -> - ?ist:Tacinterp.interp_sign -> - [> `EConstr of 'a * 'b * EConstr.t ] -> - Ssrast.ssripat option -> - Tacmach.tactic -> - bool -> - Ssrast.ssrhyp list -> - Goal.goal Evd.sigma -> Goal.goal list Evd.sigma - -(* "move=> top; tac top; clear top" respecting the speed *) -val with_top : (EConstr.t -> v82tac) -> tac_ctx tac_a + Putting these two features in the same file lets one hide much of the + interaction between [tac E:] and [=>] ([E] has to be processed by [=>], + not by [:] +*) -val ssrmovetac : - Ltac_plugin.Tacinterp.interp_sign -> - Ssrast.ssrterm list * - (Ssrast.ssripat option * - (((Ssrast.ssrdocc * Ssrmatching.cpattern) list - list * Ssrast.ssrclear) * - Ssrast.ssripats)) -> - Tacmach.tactic - -val movehnftac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma - -val with_dgens : - (Ssrast.ssrdocc * Ssrmatching.cpattern) list - list * Ssrast.ssrclear -> - ((Ssrast.ssrdocc * Ssrmatching.cpattern) list -> - Ssrast.ssrdocc * Ssrmatching.cpattern -> - Ltac_plugin.Tacinterp.interp_sign -> Tacmach.tactic) -> - Ltac_plugin.Tacinterp.interp_sign -> Tacmach.tactic - -val ssrcasetac : - Ltac_plugin.Tacinterp.interp_sign -> - Ssrast.ssrterm list * - (Ssrast.ssripat option * - (((Ssrast.ssrdocc * Ssrmatching.cpattern) list list * Ssrast.ssrclear) * - Ssrast.ssripats)) -> - Tacmach.tactic - -val ssrapplytac : - Tacinterp.interp_sign -> - Ssrast.ssrterm list * - ('a * - ((((Ssrast.ssrhyps option * Ssrmatching_plugin.Ssrmatching.occ) * - (Ssrast.ssrtermkind * Tacexpr.glob_constr_and_expr)) - list list * Ssrast.ssrhyps) * - Ssrast.ssripats)) -> - Tacmach.tactic +open Ssrast +(* The => tactical *) +val tclIPAT : ssripats -> unit Proofview.tactic + +(* As above but with the SSR exception: first case is dispatch *) +val tclIPATssr : ssripats -> unit Proofview.tactic + +(* Wrappers to deal with : and eqn generation/naming: + [tac E: gens => ipats] + where [E] is injected into [ipats] (at the right place) and [gens] are + generalized before calling [tac] *) +val ssrmovetac : ssrmovearg -> unit Proofview.tactic +val ssrsmovetac : unit Proofview.tactic +val ssrelimtac : ssrmovearg -> unit Proofview.tactic +val ssrselimtoptac : unit Proofview.tactic +val ssrcasetac : ssrmovearg -> unit Proofview.tactic +val ssrscasetoptac : unit Proofview.tactic + +(* The implementation of abstract: is half here, for the [[: var ]] + * ipat, and in ssrfwd for the integration with [have] *) +val ssrabstract : ssrdgens -> unit Proofview.tactic + +(* Handling of [[:var]], needed in ssrfwd. Since ssrfwd is still outside the + * tactic monad we export code with the V82 interface *) +module Internal : sig +val examine_abstract : + EConstr.t -> Goal.goal Evd.sigma -> EConstr.types * EConstr.t array +val pf_find_abstract_proof : + bool -> Goal.goal Evd.sigma -> Constr.constr -> Evar.t +end |