diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-05 13:15:15 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-05 13:15:15 +0100 |
| commit | 736e86e06b5831a0dd4b6a655708b4ffd2b4ee64 (patch) | |
| tree | f1f572e011f0e5e476256d58517258774bdf149e /plugins/ssr/ssrbwd.mli | |
| parent | a46a04577e34c69b42c2728ec1e0babb5be23e31 (diff) | |
| parent | 7267e31fa4456aee62a1e39dfdb7e38a8832f93f (diff) | |
Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monad
Diffstat (limited to 'plugins/ssr/ssrbwd.mli')
| -rw-r--r-- | plugins/ssr/ssrbwd.mli | 15 |
1 files changed, 4 insertions, 11 deletions
diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli index af9f7491a..eb64f337f 100644 --- a/plugins/ssr/ssrbwd.mli +++ b/plugins/ssr/ssrbwd.mli @@ -6,16 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open Ssrast +open Proofview +val apply_top_tac : unit tactic -val apply_top_tac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma - -val inner_ssrapplytac : - Ssrast.ssrterm list -> - ((Ssrast.ssrhyps option * Ssrmatching_plugin.Ssrmatching.occ) * - (Ssrast.ssrtermkind * Tacexpr.glob_constr_and_expr)) - list list -> - Ssrast.ssrhyps -> - Ssrast.ist -> - Goal.goal Evd.sigma -> Goal.goal list Evd.sigma +val inner_ssrapplytac : ssrterm list -> ssragens -> ist -> unit tactic |