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