diff options
Diffstat (limited to 'plugins/ssr/ssripats.mli')
-rw-r--r-- | plugins/ssr/ssripats.mli | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli new file mode 100644 index 00000000..89cba4be --- /dev/null +++ b/plugins/ssr/ssripats.mli @@ -0,0 +1,50 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* This file implements: + - the [=>] tactical + - the [:] pseudo-tactical for move, case, elim and abstract + + 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 [:] +*) + +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 : ssrdgens ssrmovearg -> unit Proofview.tactic +val ssrsmovetac : unit Proofview.tactic +val ssrelimtac : ssrdgens ssrmovearg -> unit Proofview.tactic +val ssrselimtoptac : unit Proofview.tactic +val ssrcasetac : ssrdgens 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 |