diff --git a/code/dawn/Dawn.v b/code/dawn/Dawn.v
index ba0be9e..a93f63b 100644
--- a/code/dawn/Dawn.v
+++ b/code/dawn/Dawn.v
@@ -131,7 +131,7 @@ Ltac2 rec solve_basic () := Control.enter (fun _ =>
   | [|- Sem_int ?vs1 apply ?vs2] => apply Sem_apply
   | [|- Sem_expr ?vs1 (e_comp ?e1 ?e2) ?vs2] => eapply Sem_e_comp; solve_basic ()
   | [|- Sem_expr ?vs1 (e_int ?e) ?vs2] => apply Sem_e_int; solve_basic ()
-  | [|- Sem_e_quote ?vs1 (e_quote ?e) ?vs2] => apply Sem_quote
+  | [|- Sem_expr ?vs1 (e_quote ?e) ?vs2] => apply Sem_e_quote
   | [_ : _ |- _] => ()
   end).