From 0caae63530538857cca322c6875ff1ca75cbe900 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sat, 25 Jan 2025 14:56:22 -0700
Subject: [PATCH] kill cram

---
 apps/coercion/tests/coercion.t/run.t                | 12 ------------
 apps/coercion/tests/coercion_open.t/run.t           |  4 ----
 apps/coercion/tests/dune                            | 13 ++++++-------
 apps/coercion/tests/setup-project.sh                |  1 -
 apps/coercion/tests/{coercion.t => }/test.v         |  0
 apps/coercion/tests/{coercion.t => }/test2.v        |  0
 .../tests/{coercion_open.t/test.v => test_open.v}   |  0
 7 files changed, 6 insertions(+), 24 deletions(-)
 delete mode 100644 apps/coercion/tests/coercion.t/run.t
 delete mode 100644 apps/coercion/tests/coercion_open.t/run.t
 delete mode 120000 apps/coercion/tests/setup-project.sh
 rename apps/coercion/tests/{coercion.t => }/test.v (100%)
 rename apps/coercion/tests/{coercion.t => }/test2.v (100%)
 rename apps/coercion/tests/{coercion_open.t/test.v => test_open.v} (100%)

diff --git a/apps/coercion/tests/coercion.t/run.t b/apps/coercion/tests/coercion.t/run.t
deleted file mode 100644
index cdfb3b585..000000000
--- a/apps/coercion/tests/coercion.t/run.t
+++ /dev/null
@@ -1,12 +0,0 @@
-  $ . ../setup-project.sh
-  $ dune build test.vo
-  true && false
-       : bool
-  natmul R n : ringType_sort R
-       : ringType_sort R
-  natmul R n : ringType_sort R
-       : ringType_sort R
-  $ dune build test2.vo
-  true : bool
-       : bool
-
diff --git a/apps/coercion/tests/coercion_open.t/run.t b/apps/coercion/tests/coercion_open.t/run.t
deleted file mode 100644
index 333c9552c..000000000
--- a/apps/coercion/tests/coercion_open.t/run.t
+++ /dev/null
@@ -1,4 +0,0 @@
-  $ . ../setup-project.sh
-  $ dune build test.vo
-  1
-       : nat
diff --git a/apps/coercion/tests/dune b/apps/coercion/tests/dune
index c49811c04..5d0075e46 100644
--- a/apps/coercion/tests/dune
+++ b/apps/coercion/tests/dune
@@ -1,7 +1,6 @@
-(cram
- (applies_to :whole_subtree)
- (deps
-  %{bin:coqc}
-  %{bin:coqdep}
-  (package coq-elpi)
-  setup-project.sh))
+(coq.theory
+ (name elpi.apps.coercion.tests)
+ (package coq-elpi-tests)
+ (theories elpi elpi.apps.coercion))
+
+(include_subdirs qualified)
diff --git a/apps/coercion/tests/setup-project.sh b/apps/coercion/tests/setup-project.sh
deleted file mode 120000
index c0d2a8f89..000000000
--- a/apps/coercion/tests/setup-project.sh
+++ /dev/null
@@ -1 +0,0 @@
-../../../etc/setup-project.sh
\ No newline at end of file
diff --git a/apps/coercion/tests/coercion.t/test.v b/apps/coercion/tests/test.v
similarity index 100%
rename from apps/coercion/tests/coercion.t/test.v
rename to apps/coercion/tests/test.v
diff --git a/apps/coercion/tests/coercion.t/test2.v b/apps/coercion/tests/test2.v
similarity index 100%
rename from apps/coercion/tests/coercion.t/test2.v
rename to apps/coercion/tests/test2.v
diff --git a/apps/coercion/tests/coercion_open.t/test.v b/apps/coercion/tests/test_open.v
similarity index 100%
rename from apps/coercion/tests/coercion_open.t/test.v
rename to apps/coercion/tests/test_open.v