diff --git a/artifact-clean.zip b/artifact-clean.zip
index 47e1576..da4369d 100644
Binary files a/artifact-clean.zip and b/artifact-clean.zip differ
diff --git a/examples/Vector_tuple.v b/examples/Vector_tuple.v
index 1d14fb6..8b87a16 100644
--- a/examples/Vector_tuple.v
+++ b/examples/Vector_tuple.v
@@ -258,16 +258,10 @@ Trocq Use Param_const.
 Trocq Use Param01_paths.
 
 Lemma head_const' : forall {n : nat} (z : Zp), head (const z (S n)) = z.
-Proof. trocq. intro n. apply head_const. Qed.
+Proof. trocq; exact: @head_const. Qed.
 
 End HeadConst.
 
-
-
-(* bug *)
-
-Module bug.
-
 Definition cons {A : Type} {n : nat} (a : A) (t : tuple A n) : tuple A (S n) := (t, a).
 
 Definition Param_cons
@@ -292,16 +286,6 @@ Defined.
 Trocq Use SR.
 Trocq Use Param_cons.
 
-Lemma append_comm_cons : forall {A : Type} {n1 n2 : nat}
-    (v1 : tuple A n1) (v2 : tuple A n2) (a : A),
-  @paths (tuple A (S (n1 + n2))) (cons a (append v1 v2)) (append (cons a v1) v2).
-Proof.
-Fail Timeout 1 trocq.
-  (* apply Vector.append_comm_cons. *)
-Abort.
-
-End bug.
-
 (* bounded nat and bitvector *)
 (* NB: we can use transitivity to make the proofs here too *)
 
diff --git a/theories/Param.v b/theories/Param.v
index 3ad83f3..a1a8c1a 100644
--- a/theories/Param.v
+++ b/theories/Param.v
@@ -155,7 +155,7 @@ Elpi Accumulate lp:{{
 }}.
 
 Elpi Accumulate lp:{{
-  solve InitialGoal NewGoals :- debug dbg.full => std.do! [
+  solve InitialGoal NewGoals :- debug dbg.none => std.do! [
     InitialGoal = goal _Context _ G _ [],
     util.when-debug dbg.full (coq.say "goal" G),
     translate-goal G (pc map0 map1) G' GR,