From ea4f6d3219d0237ff4d181f34874ae5d080c1f20 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Tue, 9 Jan 2024 10:36:24 +0100
Subject: [PATCH] fix Elpi Typecheck program

---
 _CoqProject.test           |  3 ++-
 src/coq_elpi_vernacular.ml |  2 +-
 tests/test_checker.v       | 19 +++++++++++++++++++
 3 files changed, 22 insertions(+), 2 deletions(-)
 create mode 100644 tests/test_checker.v

diff --git a/_CoqProject.test b/_CoqProject.test
index 8510ba804..266fcb992 100644
--- a/_CoqProject.test
+++ b/_CoqProject.test
@@ -55,4 +55,5 @@ tests/test_link_order_import3.v
 tests/test_query_extra_dep.v
 tests/test_toposort.v
 tests/test_synterp.v
-tests/test_grafting.v
\ No newline at end of file
+tests/test_grafting.v
+tests/test_checker.v
diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
index dc41a2119..ea578e236 100644
--- a/src/coq_elpi_vernacular.ml
+++ b/src/coq_elpi_vernacular.ml
@@ -286,7 +286,7 @@ let set_current_program n =
   current_program := Some n
 
 let typecheck_program ?program () =
-  match !current_program with
+  match Option.append program !current_program with
   | None -> ()
   | Some program ->
       let elpi = P.ensure_initialized () in
diff --git a/tests/test_checker.v b/tests/test_checker.v
new file mode 100644
index 000000000..e39000196
--- /dev/null
+++ b/tests/test_checker.v
@@ -0,0 +1,19 @@
+From elpi Require Import elpi.
+
+Elpi Command foo.
+Elpi Accumulate lp:{{
+pred p i:int.
+p 0 0.
+
+}}.
+Fail Elpi Typecheck.
+
+Elpi Command bar.
+Elpi Accumulate lp:{{
+pred p i:int.
+p 0.
+
+}}.
+Elpi Typecheck.
+
+Fail Elpi Typecheck foo.