Remove reference to Int31 in Grab88v819 (#12)

JasonGross · Oct 6, 2023 · bbe2c4c · bbe2c4c
1 parent 8648113
commit bbe2c4c
Show file tree

Hide file tree

Showing 3 changed files with 0 additions and 3 deletions.
diff --git a/compatibility/Coq__8_19__Compat.v b/compatibility/Coq__8_19__Compat.v
@@ -21,7 +21,6 @@ Require Coq.Numbers.Cyclic.Int63.Uint63.
 Number Notation BinNums.Z BinIntDef.Z.of_num_int BinIntDef.Z.to_num_int : Z_scope.
 Number Notation BinNums.positive BinPosDef.Pos.of_num_int BinPosDef.Pos.to_num_int : positive_scope.
 Number Notation BinNums.N BinNatDef.N.of_num_int BinNatDef.N.to_num_int : N_scope.
-Number Notation Int31.int31 Int31.phi_inv_nonneg Int31.phi : int31_scope.
 
 Local Set Warnings "-deprecated".
 Global Set Firstorder Solver auto with *.

diff --git a/compatibility/Coq__master__Compat.v b/compatibility/Coq__master__Compat.v
@@ -21,7 +21,6 @@ Require Coq.Numbers.Cyclic.Int63.Uint63.
 Number Notation BinNums.Z BinIntDef.Z.of_num_int BinIntDef.Z.to_num_int : Z_scope.
 Number Notation BinNums.positive BinPosDef.Pos.of_num_int BinPosDef.Pos.to_num_int : positive_scope.
 Number Notation BinNums.N BinNatDef.N.of_num_int BinNatDef.N.to_num_int : N_scope.
-Number Notation Int31.int31 Int31.phi_inv_nonneg Int31.phi : int31_scope.
 
 Local Set Warnings "-deprecated".
 Global Set Firstorder Solver auto with *.

diff --git a/compatibility/fragments/Grab88v819.v b/compatibility/fragments/Grab88v819.v
@@ -19,7 +19,6 @@ Require Coq.Numbers.Cyclic.Int63.Uint63.
 Number Notation BinNums.Z BinIntDef.Z.of_num_int BinIntDef.Z.to_num_int : Z_scope.
 Number Notation BinNums.positive BinPosDef.Pos.of_num_int BinPosDef.Pos.to_num_int : positive_scope.
 Number Notation BinNums.N BinNatDef.N.of_num_int BinNatDef.N.to_num_int : N_scope.
-Number Notation Int31.int31 Int31.phi_inv_nonneg Int31.phi : int31_scope.
 
 Local Set Warnings "-deprecated".
 Global Set Firstorder Solver auto with *.