From 87d0560dceda323cdb3e664d8f5e0083aa01fdd6 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Fri, 26 Jul 2024 22:32:00 +0200 Subject: [PATCH] make key have sentences transparent to enable extraction without nontrivial sort polymorphism error --- theories/Examples/Calculator/DelegatingCalculatorServer.v | 6 +++--- theories/Examples/Calculator/SimpleCalculatorApp.v | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) 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.