Merge pull request #983 from Villetaneuse/remove_Int31

Remove Int31
MetaCoq · Oct 1, 2023 · 573587b · 573587b
2 parents cde7d00 + c448027
commit 573587b
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 10 deletions.
diff --git a/quotation/theories/ToPCUIC/Coq/Numbers.v b/quotation/theories/ToPCUIC/Coq/Numbers.v
@@ -1,9 +1,11 @@
 From Coq.Numbers Require Import BinNums DecimalFacts HexadecimalFacts
-     Cyclic.Int63.PrimInt63 Cyclic.Int31.Int31
+     Cyclic.Int63.PrimInt63 Cyclic.Int63.Uint63
      Cyclic.Abstract.CyclicAxioms
      Cyclic.Abstract.DoubleType
      Cyclic.Abstract.CarryType
 .
+
+From Coq Require Import ZArith.
 From MetaCoq.Quotation.ToPCUIC Require Import Coq.Init.
 
 #[export] Instance quote_positive : ground_quotable positive := ltac:(induction 1; exact _).
@@ -24,14 +26,10 @@ Module Export Numbers.
   Module Export HexadecimalFacts.
     #[export] Instance quote_digits : ground_quotable HexadecimalFacts.digits := ltac:(destruct 1; exact _).
   End HexadecimalFacts.
-  Module Export Int31.
-    #[export] Instance quote_digits : ground_quotable Int31.digits := ltac:(destruct 1; exact _).
-  End Int31.
 End Numbers.
 
 #[export] Instance quote_int : ground_quotable int := fun i => PCUICAst.tInt i.
 #[export] Instance quote_pos_neg_int63 : ground_quotable pos_neg_int63 := ltac:(destruct 1; exact _).
 #[export] Instance quote_int_wrapper : ground_quotable int_wrapper := ltac:(destruct 1; exact _).
-#[export] Instance quote_int31 : ground_quotable int31 := ltac:(destruct 1; exact _).
 #[export] Instance quote_zn2z {znz} {qznz : quotation_of znz} {quoteznz : ground_quotable znz} : ground_quotable (zn2z znz) := ltac:(destruct 1; exact _).
 #[export] Instance quote_carry {A} {qA : quotation_of A} {quoteA : ground_quotable A} : ground_quotable (carry A) := ltac:(destruct 1; exact _).
diff --git a/quotation/theories/ToTemplate/Coq/Numbers.v b/quotation/theories/ToTemplate/Coq/Numbers.v
@@ -1,9 +1,10 @@
 From Coq.Numbers Require Import BinNums DecimalFacts HexadecimalFacts
-     Cyclic.Int63.PrimInt63 Cyclic.Int31.Int31
+     Cyclic.Int63.PrimInt63 Cyclic.Int63.Uint63
      Cyclic.Abstract.CyclicAxioms
      Cyclic.Abstract.DoubleType
      Cyclic.Abstract.CarryType
 .
+From Coq Require Import ZArith.
 From MetaCoq.Quotation.ToTemplate Require Import Coq.Init.
 
 #[export] Instance quote_positive : ground_quotable positive := ltac:(induction 1; exact _).
@@ -24,14 +25,10 @@ Module Export Numbers.
   Module Export HexadecimalFacts.
     #[export] Instance quote_digits : ground_quotable HexadecimalFacts.digits := ltac:(destruct 1; exact _).
   End HexadecimalFacts.
-  Module Export Int31.
-    #[export] Instance quote_digits : ground_quotable Int31.digits := ltac:(destruct 1; exact _).
-  End Int31.
 End Numbers.
 
 #[export] Instance quote_int : ground_quotable int := fun i => Ast.tInt i.
 #[export] Instance quote_pos_neg_int63 : ground_quotable pos_neg_int63 := ltac:(destruct 1; exact _).
 #[export] Instance quote_int_wrapper : ground_quotable int_wrapper := ltac:(destruct 1; exact _).
-#[export] Instance quote_int31 : ground_quotable int31 := ltac:(destruct 1; exact _).
 #[export] Instance quote_zn2z {znz} {qznz : quotation_of znz} {quoteznz : ground_quotable znz} : ground_quotable (zn2z znz) := ltac:(destruct 1; exact _).
 #[export] Instance quote_carry {A} {qA : quotation_of A} {quoteA : ground_quotable A} : ground_quotable (carry A) := ltac:(destruct 1; exact _).