From 25143e0945d3155c568f1d7979c56adc4b068f3f Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@gmail.com>
Date: Fri, 19 Apr 2019 09:46:38 -0400
Subject: [PATCH] fixixing so that installation works.

---
 .gitignore                                    | 2 +-
 _CoqProject                                   | 7 ++++---
 src/{ltac_iter_plugin.ml4 => g_ltac_iter.ml4} | 2 +-
 src/ltac_iter.mlpack                          | 1 +
 test-suite/example.v                          | 2 +-
 theories/LtacIter.v                           | 2 +-
 6 files changed, 9 insertions(+), 7 deletions(-)
 rename src/{ltac_iter_plugin.ml4 => g_ltac_iter.ml4} (99%)
 create mode 100644 src/ltac_iter.mlpack

diff --git a/.gitignore b/.gitignore
index a7bd388..2f9caf5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -11,7 +11,7 @@
 *.vi
 *.glob
 *.v.d
-*.ml4.d
+*.d
 *.aux
 Makefile.coq
 Makefile.coq.conf
diff --git a/_CoqProject b/_CoqProject
index 62dc2e7..8255831 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,7 +1,8 @@
+-R theories LtacIter
 -I src
--Q theories LtacIter
 
-src/ltac_iter_plugin.ml4
+src/g_ltac_iter.ml4
+src/ltac_iter.mlpack
 theories/LtacIter.v
 
-test-suite/example.v
+# test-suite/example.v
diff --git a/src/ltac_iter_plugin.ml4 b/src/g_ltac_iter.ml4
similarity index 99%
rename from src/ltac_iter_plugin.ml4
rename to src/g_ltac_iter.ml4
index 07508c4..8d2fd2f 100644
--- a/src/ltac_iter_plugin.ml4
+++ b/src/g_ltac_iter.ml4
@@ -8,7 +8,7 @@ open Tacinterp
 open Tacarg
 
 
-DECLARE PLUGIN "ltac_iter_plugin"
+DECLARE PLUGIN "ltac_iter"
 
 
 module WITH_DB =
diff --git a/src/ltac_iter.mlpack b/src/ltac_iter.mlpack
new file mode 100644
index 0000000..4638449
--- /dev/null
+++ b/src/ltac_iter.mlpack
@@ -0,0 +1 @@
+G_ltac_iter
\ No newline at end of file
diff --git a/test-suite/example.v b/test-suite/example.v
index 186de35..048cee0 100644
--- a/test-suite/example.v
+++ b/test-suite/example.v
@@ -9,7 +9,7 @@ Axiom pfFalse : True.
 Hint Resolve pfTrue pfFalse : test_db.
 
 Goal True.
-  let k l := pose l in
+  let k l := (idtac l) in
   foreach [ rev db:test_db ] k.
   exact I.
 Defined.
diff --git a/theories/LtacIter.v b/theories/LtacIter.v
index 9dc5a07..12efa5b 100644
--- a/theories/LtacIter.v
+++ b/theories/LtacIter.v
@@ -1 +1 @@
-Declare ML Module "ltac_iter_plugin".
\ No newline at end of file
+Declare ML Module "ltac_iter".
\ No newline at end of file