Skip to content

Commit

Permalink
fix Elpi Typecheck program
Browse files Browse the repository at this point in the history
  • Loading branch information
gares committed Feb 8, 2024
1 parent c8bff49 commit 7c9d321
Show file tree
Hide file tree
Showing 3 changed files with 21 additions and 1 deletion.
1 change: 1 addition & 0 deletions _CoqProject.test
Original file line number Diff line number Diff line change
Expand Up @@ -55,3 +55,4 @@ tests/test_link_order_import3.v
tests/test_query_extra_dep.v
tests/test_toposort.v
tests/test_synterp.v
tests/test_checker.v
2 changes: 1 addition & 1 deletion src/coq_elpi_vernacular.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
19 changes: 19 additions & 0 deletions tests/test_checker.v
Original file line number Diff line number Diff line change
@@ -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.

0 comments on commit 7c9d321

Please sign in to comment.