blob: 80134afdf55cf55249844d19a849594d849e6271 (
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
|
(***************************************************************************)
(* This is part of aac_tactics, it is distributed under the terms of the *)
(* GNU Lesser General Public License version 3 *)
(* (see file LICENSE for more details) *)
(* *)
(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *)
(***************************************************************************)
(** aac_rewrite -- rewriting modulo A or AC*)
val aac_reflexivity : Coq.goal_sigma -> Proof_type.goal list Evd.sigma
val aac_normalise : Coq.goal_sigma -> Proof_type.goal list Evd.sigma
val aac_rewrite :
args:(string * int) list ->
?abort:bool ->
EConstr.constr ->
?l2r:bool ->
?show:bool ->
?strict:bool -> ?extra:EConstr.t -> Proof_type.tactic
val add : string -> 'a -> (string * 'a) list -> (string * 'a) list
val pr_aac_args : 'a -> 'b -> 'c -> (string * int) list -> Pp.t
|
