remove generic parameter for ActiveVestingContractAbortsIf as it overrides the VestingContract type (aptos-labs#16054)

Author: mkurnikov

aptos-move/framework/aptos-framework/doc/vesting.md

@@ -3807,7 +3807,7 @@ This address should be deterministic for the same admin and vesting contract cre
 
 <pre><code><b>schema</b> <a href="vesting.md#0x1_vesting_TotalAccumulatedRewardsAbortsIf">TotalAccumulatedRewardsAbortsIf</a> {
     vesting_contract_address: <b>address</b>;
-    <b>include</b> <a href="vesting.md#0x1_vesting_ActiveVestingContractAbortsIf">ActiveVestingContractAbortsIf</a>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;{contract_address: vesting_contract_address};
+    <b>include</b> <a href="vesting.md#0x1_vesting_ActiveVestingContractAbortsIf">ActiveVestingContractAbortsIf</a>{contract_address: vesting_contract_address};
     <b>let</b> vesting_contract = <b>global</b>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;(vesting_contract_address);
     <b>let</b> staker = vesting_contract_address;
     <b>let</b> operator = vesting_contract.staking.operator;
@@ -3881,7 +3881,7 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
-<pre><code><b>include</b> <a href="vesting.md#0x1_vesting_ActiveVestingContractAbortsIf">ActiveVestingContractAbortsIf</a>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;{contract_address: vesting_contract_address};
+<pre><code><b>include</b> <a href="vesting.md#0x1_vesting_ActiveVestingContractAbortsIf">ActiveVestingContractAbortsIf</a>{contract_address: vesting_contract_address};
 </code></pre>
 
 
@@ -3908,7 +3908,7 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 <pre><code><b>pragma</b> opaque;
-<b>include</b> <a href="vesting.md#0x1_vesting_ActiveVestingContractAbortsIf">ActiveVestingContractAbortsIf</a>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;{contract_address: vesting_contract_address};
+<b>include</b> <a href="vesting.md#0x1_vesting_ActiveVestingContractAbortsIf">ActiveVestingContractAbortsIf</a>{contract_address: vesting_contract_address};
 <b>ensures</b> [abstract] result == <a href="vesting.md#0x1_vesting_spec_shareholder">spec_shareholder</a>(vesting_contract_address, shareholder_or_beneficiary);
 </code></pre>
 
@@ -4062,7 +4062,7 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 <pre><code><b>pragma</b> verify = <b>false</b>;
-<b>include</b> <a href="vesting.md#0x1_vesting_ActiveVestingContractAbortsIf">ActiveVestingContractAbortsIf</a>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;;
+<b>include</b> <a href="vesting.md#0x1_vesting_ActiveVestingContractAbortsIf">ActiveVestingContractAbortsIf</a>;
 <b>let</b> vesting_contract = <b>global</b>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;(contract_address);
 <b>include</b> <a href="vesting.md#0x1_vesting_WithdrawStakeAbortsIf">WithdrawStakeAbortsIf</a> { vesting_contract };
 </code></pre>
@@ -4098,7 +4098,7 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 <pre><code><b>pragma</b> verify = <b>false</b>;
-<b>include</b> <a href="vesting.md#0x1_vesting_ActiveVestingContractAbortsIf">ActiveVestingContractAbortsIf</a>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;;
+<b>include</b> <a href="vesting.md#0x1_vesting_ActiveVestingContractAbortsIf">ActiveVestingContractAbortsIf</a>;
 <b>let</b> vesting_contract = <b>global</b>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;(contract_address);
 <b>include</b> <a href="vesting.md#0x1_vesting_WithdrawStakeAbortsIf">WithdrawStakeAbortsIf</a> { vesting_contract };
 </code></pre>
@@ -4475,7 +4475,7 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
-<pre><code><b>include</b> <a href="vesting.md#0x1_vesting_ActiveVestingContractAbortsIf">ActiveVestingContractAbortsIf</a>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;;
+<pre><code><b>include</b> <a href="vesting.md#0x1_vesting_ActiveVestingContractAbortsIf">ActiveVestingContractAbortsIf</a>;
 </code></pre>
 
 
@@ -4635,7 +4635,7 @@ This address should be deterministic for the same admin and vesting contract cre
 <a id="0x1_vesting_ActiveVestingContractAbortsIf"></a>
 
 
-<pre><code><b>schema</b> <a href="vesting.md#0x1_vesting_ActiveVestingContractAbortsIf">ActiveVestingContractAbortsIf</a>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt; {
+<pre><code><b>schema</b> <a href="vesting.md#0x1_vesting_ActiveVestingContractAbortsIf">ActiveVestingContractAbortsIf</a> {
     contract_address: <b>address</b>;
     // This enforces <a id="high-level-spec-5" href="#high-level-req">high-level requirement 5</a>:
     <b>aborts_if</b> !<b>exists</b>&lt;<a href="vesting.md#0x1_vesting_VestingContract">VestingContract</a>&gt;(contract_address);

aptos-move/framework/aptos-framework/sources/vesting.spec.move

@@ -171,7 +171,7 @@ spec aptos_framework::vesting {
         vesting_contract_address: address;
 
 
-        include ActiveVestingContractAbortsIf<VestingContract>{contract_address: vesting_contract_address};
+        include ActiveVestingContractAbortsIf{contract_address: vesting_contract_address};
         let vesting_contract = global<VestingContract>(vesting_contract_address);
 
         let staker = vesting_contract_address;
@@ -228,14 +228,14 @@ spec aptos_framework::vesting {
     }
 
     spec shareholders(vesting_contract_address: address): vector<address> {
-        include ActiveVestingContractAbortsIf<VestingContract>{contract_address: vesting_contract_address};
+        include ActiveVestingContractAbortsIf{contract_address: vesting_contract_address};
     }
 
     spec fun spec_shareholder(vesting_contract_address: address, shareholder_or_beneficiary: address): address;
 
     spec shareholder(vesting_contract_address: address, shareholder_or_beneficiary: address): address {
         pragma opaque;
-        include ActiveVestingContractAbortsIf<VestingContract>{contract_address: vesting_contract_address};
+        include ActiveVestingContractAbortsIf{contract_address: vesting_contract_address};
         ensures [abstract] result == spec_shareholder(vesting_contract_address, shareholder_or_beneficiary);
     }
 
@@ -314,7 +314,7 @@ spec aptos_framework::vesting {
     spec distribute(contract_address: address) {
         // TODO: Can't handle abort in loop.
         pragma verify = false;
-        include ActiveVestingContractAbortsIf<VestingContract>;
+        include ActiveVestingContractAbortsIf;
 
         let vesting_contract = global<VestingContract>(contract_address);
         include WithdrawStakeAbortsIf { vesting_contract };
@@ -329,7 +329,7 @@ spec aptos_framework::vesting {
     spec terminate_vesting_contract(admin: &signer, contract_address: address) {
         // TODO: Calls `staking_contract::distribute` which is not verified.
         pragma verify = false;
-        include ActiveVestingContractAbortsIf<VestingContract>;
+        include ActiveVestingContractAbortsIf;
 
         let vesting_contract = global<VestingContract>(contract_address);
         include WithdrawStakeAbortsIf { vesting_contract };
@@ -552,7 +552,7 @@ spec aptos_framework::vesting {
     }
 
     spec assert_active_vesting_contract(contract_address: address) {
-        include ActiveVestingContractAbortsIf<VestingContract>;
+        include ActiveVestingContractAbortsIf;
     }
 
     spec unlock_stake(vesting_contract: &VestingContract, amount: u64) {
@@ -649,7 +649,7 @@ spec aptos_framework::vesting {
         aborts_if signer::address_of(admin) != vesting_contract.admin;
     }
 
-    spec schema ActiveVestingContractAbortsIf<VestingContract> {
+    spec schema ActiveVestingContractAbortsIf {
         contract_address: address;
         /// [high-level-spec-5]
         aborts_if !exists<VestingContract>(contract_address);