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
68
69
70
71
72
73
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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 : Id.t -> ((ssrfwdfmt * (Ssrmatching_plugin.Ssrmatching.cpattern * ast_closure_term option)) * ssrdocc) -> unit Proofview.tactic
val ssrposetac : Id.t * (ssrfwdfmt * ast_closure_term) -> unit Proofview.tactic
val havetac : ist ->
bool *
((((Ssrast.ssrclear option * Ssrast.ssripat list) * Ssrast.ssripats) *
Ssrast.ssripats) *
(((Ssrast.ssrfwdkind * 'a) * ast_closure_term) *
(bool * Tacinterp.Value.t option list))) ->
bool ->
bool -> unit Proofview.tactic
type cut_kind = Have | HaveTransp | Suff
val basecuttac : cut_kind -> EConstr.t -> unit Proofview.tactic
val basesufftac : EConstr.t -> unit Proofview.tactic
val wlogtac :
Ltac_plugin.Tacinterp.interp_sign ->
((Ssrast.ssrclear option * Ssrast.ssripats) * 'a) * 'b ->
(Ssrast.ssrhyps *
((Ssrast.ssrhyp_or_id * string) *
Ssrmatching_plugin.Ssrmatching.cpattern option)
option)
list *
('c *
ast_closure_term) ->
Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint ->
bool ->
[< `Gen of Names.Id.t option option | `NoGen > `NoGen ] ->
unit Proofview.tactic
val sufftac :
Ssrast.ist ->
(((Ssrast.ssrclear option * Ssrast.ssripats) * Ssrast.ssripat list) *
Ssrast.ssripat list) *
(('a *
ast_closure_term) *
(bool * Tacinterp.Value.t option list)) ->
unit Proofview.tactic
(* pad_intro (by default false) indicates whether the intro-pattern
"=> i..." must be turned into "=> [i...|i...|i...|]" (n+1 branches,
assuming there are n provided tactics in the ssrhint argument
"do [...|...|...]"; it is useful when the intro-pattern is "=> *").
Otherwise, "=> i..." is turned into "=> [i...|]". *)
val undertac :
?pad_intro:bool ->
Ltac_plugin.Tacinterp.interp_sign ->
Ssrast.ssripats option -> Ssrequality.ssrrwarg ->
Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic
val overtac :
unit Proofview.tactic
|
