summaryrefslogtreecommitdiff
path: root/aac_rewrite.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-28 13:45:46 +0000
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-28 13:45:46 +0000
commitf6c35088fc20b534aac0b92df7cb9750d2b68b46 (patch)
treeb6927cf8b82cf1b038f3915679a4c590c4435afa /aac_rewrite.mli
parenta8c0742d53ca8802a3032d801e4a5e169851078e (diff)
parent76f9b4cdc5693a6313961e2f91b39ba311857e72 (diff)
Merge tag 'upstream/8.6.1'
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.*)