diff --git a/theories/Examples/Calculator/DelegatingCalculatorServer.v b/theories/Examples/Calculator/DelegatingCalculatorServer.v
index a533e62..36132b0 100644
--- a/theories/Examples/Calculator/DelegatingCalculatorServer.v
+++ b/theories/Examples/Calculator/DelegatingCalculatorServer.v
@@ -91,21 +91,21 @@ Proof. by move=>????; rewrite dom0. Qed.
 
 Next Obligation.
 rewrite -(unitR V)/V.
-have V: valid (W1 \+ W2 \+ Unit) by rewrite unitR validV.
+have @V: valid (W1 \+ W2 \+ Unit) by rewrite unitR validV.
 apply: (injectL V); do?[apply: hook_complete_unit | apply: hooks_consistent_unit].
 by move=>??????; rewrite dom0.
 Defined.
 
 Next Obligation.
 rewrite -(unitR V)/V.
-have V: valid (W1 \+ W2 \+ Unit) by rewrite unitR validV.
+have @V: valid (W1 \+ W2 \+ Unit) by rewrite unitR validV.
 apply: (injectR V); do?[apply: hook_complete_unit | apply: hooks_consistent_unit].
 by move=>??????; rewrite dom0.
 Qed.
 
 Next Obligation.
 rewrite -(unitR V)/V.
-have V: valid (W1 \+ W2 \+ Unit) by rewrite unitR validV.
+have @V: valid (W1 \+ W2 \+ Unit) by rewrite unitR validV.
 apply: (injectL V); do?[apply: hook_complete_unit | apply: hooks_consistent_unit].
 by move=>??????; rewrite dom0.
 Defined.
diff --git a/theories/Examples/Calculator/SimpleCalculatorApp.v b/theories/Examples/Calculator/SimpleCalculatorApp.v
index 969df77..b7209f8 100644
--- a/theories/Examples/Calculator/SimpleCalculatorApp.v
+++ b/theories/Examples/Calculator/SimpleCalculatorApp.v
@@ -223,7 +223,7 @@ Program Definition client_run (u : unit) :
 
 Next Obligation.
 rewrite -(unitR V)/V.
-have V: valid (W1 \+ W2 \+ Unit) by rewrite unitR validV.
+have @V: valid (W1 \+ W2 \+ Unit) by rewrite unitR validV.
 apply: (injectL V); do?[apply: hook_complete_unit | apply: hooks_consistent_unit].
 by move=>??????; rewrite dom0.
 Qed.
@@ -282,7 +282,7 @@ Program Definition server2_run (u : unit) :
 
 Next Obligation.
 rewrite -(unitR V)/V.
-have V: valid (W1 \+ W2 \+ Unit) by rewrite unitR validV.
+have @V: valid (W1 \+ W2 \+ Unit) by rewrite unitR validV.
 apply: (injectR V); do?[apply: hook_complete_unit | apply: hooks_consistent_unit].
 by move=>??????; rewrite dom0.
 Qed.