Merge pull request #18 from DistributedComponents/transparent-have

make key have sentences transparent to enable extraction in 8.20

Author: palmskog

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.

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.