summaryrefslogtreecommitdiff
path: root/aac_rewrite.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-28 13:43:01 +0000
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-28 13:43:01 +0000
commit76f9b4cdc5693a6313961e2f91b39ba311857e72 (patch)
treed0bc68aa8ed8da41ecf7250883913f531bc66ef0 /aac_rewrite.mli
parent1117d2e4a00debfbfa0157cc3e780916df72c26b (diff)
New upstream version 8.6.1
Diffstat (limited to 'aac_rewrite.mli')
-rw-r--r--aac_rewrite.mli9
1 files changed, 9 insertions, 0 deletions
diff --git a/aac_rewrite.mli b/aac_rewrite.mli
new file mode 100644
index 0000000..d195075
--- /dev/null
+++ b/aac_rewrite.mli
@@ -0,0 +1,9 @@
+(***************************************************************************)
+(* 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. *)
+(***************************************************************************)
+
+(** Definition of the tactics, and corresponding Coq grammar entries.*)