Merge pull request #906 from JasonGross/coq-8.16+remove-dead-quotation-code

Remove some duplicate code in quotation

Author: tabareau

quotation/theories/ToTemplate/Coq/FSets.v

@@ -1,5 +1,5 @@
 From Coq Require Import Structures.Equalities Structures.OrdersAlt FMapInterface FMapList FMapAVL FMapFullAVL FMapFacts.
-From MetaCoq.Utils Require Import MCUtils.
+From MetaCoq.Utils Require Import MCUtils MCFSets.
 From MetaCoq.Quotation.ToTemplate Require Import Init.
 From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Numbers Coq.Init Coq.Lists.
 From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import OrdersAlt.Sig.

quotation/theories/ToTemplate/Coq/MSets.v

@@ -1,4 +1,5 @@
 From Coq Require Import MSetInterface MSetList MSetAVL MSetFacts MSetProperties MSetDecide.
+From MetaCoq.Utils Require Import MCMSets.
 From MetaCoq.Quotation.ToTemplate Require Import Init.
 From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Numbers Coq.Init Coq.Lists.
 From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import Orders.Sig.

quotation/theories/ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.v

@@ -1,15 +1,14 @@
 From Coq.FSets Require Import FMapAVL.
 From Coq.Structures Require Import Equalities OrdersAlt.
+From MetaCoq.Utils Require Import MCFSets.
 From MetaCoq.Quotation.ToTemplate Require Import Init.
 From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import OrdersAlt.Sig.
 From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.FSets Require Import FMapList.Sig.
 Import List.ListNotations.
 Local Open Scope list_scope.
 
 Module FMapAVL.
-  Module Type MakeSig (T : OrderedTypeOrig) := Nop <+ FMapAVL.Make T.
-
-  Module Type QuotationOfMake (T : OrderedTypeOrig) (M : MakeSig T).
+  Module Type QuotationOfMake (T : OrderedTypeOrig) (M : FMapAVL.MakeSig T).
     Module qRaw.
       Module qProofs.
         Module qMX := Nop <+ QuotationOfOrderedTypeOrigFacts T M.Raw.Proofs.MX.

quotation/theories/ToTemplate/QuotationOf/Coq/FSets/FMapFacts/Sig.v

@@ -1,10 +1,9 @@
 From Coq.FSets Require Import FMapFacts.
 From Coq.Structures Require Import Orders.
+From MetaCoq.Utils Require Import MCFSets.
 From MetaCoq.Quotation.ToTemplate Require Import Init.
 
 Module Export FSets.
-  Module Type WFacts_funSig (E : DecidableTypeOrig) (M : WSfun E) := Nop <+ WFacts_fun E M.
-
   Module Type QuotationOfWFacts_fun (E : DecidableTypeOrig) (M : WSfun E) (F : WFacts_funSig E M).
     MetaCoq Run (tmDeclareQuotationOfModule everything (Some export) "F").
   End QuotationOfWFacts_fun.

quotation/theories/ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.v

@@ -1,14 +1,13 @@
 From Coq.FSets Require Import FMapList.
 From Coq.Structures Require Import Equalities OrdersAlt.
+From MetaCoq.Utils Require Import MCFSets.
 From MetaCoq.Quotation.ToTemplate Require Import Init.
 From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import OrdersAlt.Sig.
 Import List.ListNotations.
 Local Open Scope list_scope.
 
 Module FMapList.
-  Module Type RawSig (T : OrderedTypeOrig) := Nop <+ FMapList.Raw T.
-
-  Module Type QuotationOfRaw (T : OrderedTypeOrig) (M : RawSig T).
+  Module Type QuotationOfRaw (T : OrderedTypeOrig) (M : FMapList.RawSig T).
     Module qMX := Nop <+ QuotationOfOrderedTypeOrigFacts T M.MX.
     Module qPX := Nop <+ QuotationOfKeyOrderedTypeOrig T M.PX.
     Export (hints) qMX qPX.

quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.v

@@ -1,11 +1,10 @@
 From Coq.Structures Require Import Orders.
 From Coq.MSets Require Import MSetAVL.
+From MetaCoq.Utils Require Import MCMSets.
 From MetaCoq.Quotation.ToTemplate Require Import Init.
 
 Module MSetAVL.
-  Module Type MakeSig (T : OrderedType) := Nop <+ MSetAVL.Make T.
-
-  Module Type QuotationOfMake (T : OrderedType) (M : MakeSig T).
+  Module Type QuotationOfMake (T : OrderedType) (M : MSetAVL.MakeSig T).
     MetaCoq Run (tmDeclareQuotationOfModule everything (Some export) "M").
   End QuotationOfMake.
 End MSetAVL.

quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetDecide/Sig.v

@@ -1,11 +1,8 @@
 From Coq.MSets Require Import MSetInterface MSetDecide.
+From MetaCoq.Utils Require Import MCMSets.
 From MetaCoq.Quotation.ToTemplate Require Import Init.
 
 Module Export MSets.
-  Module Type WDecideOnSig (E : DecidableType) (M : WSetsOn E) := Nop <+ WDecideOn E M.
-  Module Type WDecideSig (M : WSets) := Nop <+ WDecide M.
-  Module Type DecideSig (M : WSets) := Nop <+ Decide M.
-
   Module Type QuotationOfWDecideOn (E : DecidableType) (M : WSetsOn E) (F : WDecideOnSig E M).
     MetaCoq Run (tmDeclareQuotationOfModule everything (Some export) "F").
   End QuotationOfWDecideOn.

quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetFacts/Sig.v

@@ -1,11 +1,8 @@
 From Coq.MSets Require Import MSetFacts.
+From MetaCoq.Utils Require Import MCMSets.
 From MetaCoq.Quotation.ToTemplate Require Import Init.
 
 Module Export MSets.
-  Module Type WFactsOnSig (E : DecidableType) (M : WSetsOn E) := Nop <+ WFactsOn E M.
-  Module Type WFactsSig (M : WSets) := Nop <+ WFacts M.
-  Module Type FactsSig (M : WSets) := Nop <+ Facts M.
-
   Module Type QuotationOfWFactsOn (E : DecidableType) (M : WSetsOn E) (F : WFactsOnSig E M).
     MetaCoq Run (tmDeclareQuotationOfModule everything (Some export) "F").
   End QuotationOfWFactsOn.

quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetInterface/Sig.v

@@ -21,8 +21,3 @@ Module Type QuotationOfSetsOn (E : OrderedType) (Import M : SetsOn E).
   #[export] Declare Instance qchoose_spec3 : quotation_of M.choose_spec3.
 End QuotationOfSetsOn.
 Module Type QuotationOfSets (M : Sets) := QuotationOfSetsOn M.E M.
-
-Module Type UsualSets <: Sets.
-  Declare Module E : UsualOrderedType.
-  Include SetsOn E.
-End UsualSets.

quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.v

@@ -1,5 +1,6 @@
 From Coq.Structures Require Import Equalities Orders.
 From Coq.MSets Require Import MSetList.
+From MetaCoq.Utils Require Import MCMSets.
 From MetaCoq.Quotation.ToTemplate Require Import Init.
 From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.MSets Require Import MSetInterface.Sig.
 
@@ -13,15 +14,11 @@ Module Type QuotationOfSWithLeibniz (S : SWithLeibniz).
 End QuotationOfSWithLeibniz.
 
 Module MSetList.
-  Module Type MakeSig (T : OrderedType) := Nop <+ MSetList.Make T.
-
-  Module Type QuotationOfMake (T : OrderedType) (M : MakeSig T).
+  Module Type QuotationOfMake (T : OrderedType) (M : MSetList.MakeSig T).
     MetaCoq Run (tmDeclareQuotationOfModule everything (Some export) "M").
   End QuotationOfMake.
 
-  Module Type MakeWithLeibnizSig (X : OrderedTypeWithLeibniz) := Nop <+ MakeWithLeibniz X.
-
-  Module Type QuotationOfMakeWithLeibniz (T : OrderedTypeWithLeibniz) (M : MakeWithLeibnizSig T).
+  Module Type QuotationOfMakeWithLeibniz (T : OrderedTypeWithLeibniz) (M : MSetList.MakeWithLeibnizSig T).
     Include QuotationOfMake T M.
     #[export] Declare Instance qeq_leibniz_list : quotation_of M.eq_leibniz_list.
     #[export] Declare Instance qeq_leibniz : quotation_of M.eq_leibniz.