fixixing so that installation works.

gmalecha · Apr 19, 2019 · 25143e0 · 25143e0
1 parent 3dbe87d
commit 25143e0
Show file tree

Hide file tree

Showing 6 changed files with 9 additions and 7 deletions.
diff --git 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
@@ -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 → src/g_ltac_iter.ml4 b/src/ltac_iter_plugin.ml4 → 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
@@ -0,0 +1 @@
+G_ltac_iter
diff --git 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
@@ -1 +1 @@
-Declare ML Module "ltac_iter_plugin".
+Declare ML Module "ltac_iter".
-Original file line number
+Diff line change
@@ Expand Up / @@ -11,7 +11,7 @@ @@
     *.vi
     *.glob
     *.v.d
-    *.ml4.d
+    *.d
     *.aux
     Makefile.coq
     Makefile.coq.conf
@@ Expand Down @@
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		Declare ML Module "ltac_iter_plugin".
		Declare ML Module "ltac_iter".