Merge remote-tracking branch 'origin/coq-8.16' into coq-8.17

Author: mattam82

erasure/theories/EArities.v

@@ -8,7 +8,7 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils
   PCUICSR PCUICGeneration PCUICSubstitution PCUICElimination
   PCUICWeakeningEnv PCUICWeakeningEnvTyp
   PCUICWellScopedCumulativity
-  PCUICContextConversion PCUICConversion PCUICCanonicity
+  PCUICContextConversion PCUICConversion PCUICClassification
   PCUICSpine PCUICInductives PCUICInductiveInversion PCUICConfluence
   PCUICArities PCUICPrincipality.
 

erasure/theories/ErasureCorrectness.v

@@ -12,7 +12,7 @@ From MetaCoq.PCUIC Require Import PCUICTyping PCUICGlobalEnv PCUICAst
   PCUICWcbvEval PCUICSR PCUICInversion
   PCUICLiftSubst
   PCUICUnivSubstitutionConv PCUICUnivSubstitutionTyp
-  PCUICElimination PCUICCanonicity
+  PCUICElimination PCUICClassification
   PCUICUnivSubst PCUICViews
   PCUICCumulativity PCUICSafeLemmata
   PCUICArities PCUICInductiveInversion

erasure/theories/Prelim.v

@@ -6,7 +6,7 @@ From MetaCoq.PCUIC Require Import PCUICTyping PCUICAst PCUICAstUtils
      PCUICSubstitution PCUICLiftSubst PCUICClosedTyp
      PCUICReduction PCUICWcbvEval PCUICSR PCUICInversion PCUICGeneration
      PCUICContextConversion PCUICArities PCUICWellScopedCumulativity PCUICConversion
-     PCUICWeakeningEnvTyp PCUICCanonicity.
+     PCUICWeakeningEnvTyp PCUICClassification.
 From MetaCoq.SafeChecker Require Import PCUICErrors.
 From Coq Require Import Program ssreflect.
 

pcuic/_CoqProject.in

@@ -78,6 +78,7 @@ theories/PCUICInductives.v
 theories/PCUICValidity.v
 theories/PCUICInductiveInversion.v
 theories/PCUICSR.v
+theories/PCUICClassification.v
 theories/PCUICCanonicity.v
 
 theories/PCUICCSubst.v