Fix metacoq_tour

MetaCoq · Jul 22, 2024 · c6180f0 · c6180f0
1 parent 67ee744
commit c6180f0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/examples/metacoq_tour.v b/examples/metacoq_tour.v
@@ -99,7 +99,7 @@ From MetaCoq.ErasurePlugin Require Import Erasure Loader.
 
 (** Running erasure live in Coq *)
 Definition test (p : Ast.Env.program) : string :=
-  erase_and_print_template_program default_erasure_config p.
+  erase_and_print_template_program default_erasure_config [] p.
 
 MetaCoq Quote Recursively Definition zero := 0.