Merge pull request #18 from DistributedComponents/transparent-have

make key have sentences transparent to enable extraction in 8.20
DistributedComponents · Jul 26, 2024 · 4ae4c20 · 4ae4c20
2 parents df89c4a + 87d0560
commit 4ae4c20
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git 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
@@ -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.