aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr/ssrfwd.mli
blob: f5e4bd0ad1e797c4a468f972601b074f8506c0ac (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
(************************************************************************)
(*         *   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 is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)

open Names

open Ltac_plugin

open Ssrast

val ssrsettac : ist ->  Id.t -> ((ssrfwdfmt * (Ssrmatching_plugin.Ssrmatching.cpattern * ssrterm option)) * ssrdocc) -> v82tac

val ssrposetac : ist -> (Id.t * (ssrfwdfmt * ssrterm)) -> v82tac

val havetac :
           Ssrast.ist ->
           bool *
           ((((Ssrast.ssrclear * Ssrast.ssripat list) * Ssrast.ssripats) *
             Ssrast.ssripats) *
            (((Ssrast.ssrfwdkind * 'a) *
              ('b * (Glob_term.glob_constr * Constrexpr.constr_expr option))) *
             (bool * Tacinterp.Value.t option list))) ->
           bool ->
           bool -> v82tac
val ssrabstract :
           Tacinterp.interp_sign ->
           (Ssrast.ssrdocc * Ssrmatching_plugin.Ssrmatching.cpattern) list
           list * Ssrast.ssrclear -> v82tac

val basecuttac :
           string ->
           EConstr.t -> Goal.goal Evd.sigma -> Evar.t list Evd.sigma

val wlogtac :
  Ltac_plugin.Tacinterp.interp_sign ->
  ((Ssrast.ssrhyps * Ssrast.ssripats) * 'a) * 'b ->
  (Ssrast.ssrhyps *
     ((Ssrast.ssrhyp_or_id * string) *
        Ssrmatching_plugin.Ssrmatching.cpattern option)
       option)
    list *
    ('c *
       (Ssrast.ssrtermkind *
          (Glob_term.glob_constr * Constrexpr.constr_expr option))) ->
  Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint ->
  bool ->
  [< `Gen of Names.Id.t option option | `NoGen > `NoGen ] ->
  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma

val sufftac :
  Ssrast.ist ->
  (((Ssrast.ssrhyps * Ssrast.ssripats) * Ssrast.ssripat list) *
     Ssrast.ssripat list) *
    (('a *
        (Ssrast.ssrtermkind *
           (Glob_term.glob_constr * Constrexpr.constr_expr option))) *
       (bool * Tacinterp.Value.t option list)) ->
  Tacmach.tactic