Fixes after merge

Author: mattam82

erasure-plugin/theories/ErasureCorrectness.v

@@ -1153,7 +1153,7 @@ Section PCUICErase.
     set(prf := fun (n : nat) => _).
     set(prf' := fun (Σ : global_env) => _).
     unshelve eexists. intros ? ->; reflexivity.
-    epose proof (@erase_global_deps_fast_erase_global_deps (term_global_deps er') optimized_abstract_env_impl wfe (declarations p.1)) as [nin2 eq].
+    epose proof (@erase_global_deps_fast_erase_global_deps (term_global_deps er') optimized_abstract_env_impl wfe (declarations p.1) _ _ _) as [nin2 eq].
     exists nin2.
     set(prf'' := fun (Σ : global_env) => _).
     set(prf''' := ETransform.erase_pcuic_program_obligation_6 _ _ _ _ _ _).

erasure/theories/EEtaExpanded.v

@@ -458,6 +458,7 @@ Variable Σ : global_declarations.
 
 Local Unset Elimination Schemes.
 
+#[universes(template=no)]
 Inductive expanded : term -> Prop :=
 | expanded_tRel (n : nat) : expanded (tRel n)
 | expanded_tVar (id : ident) : expanded (tVar id)
@@ -477,7 +478,7 @@ Inductive expanded : term -> Prop :=
     #|args| >= cstr_arity mind cdecl ->
     Forall expanded args ->
     expanded (mkApps (tConstruct ind idx []) args)
-| expanded_tPrim p : primProp expanded p -> expanded (tPrim p)
+| expanded_tPrim p : primProp@{Set Set} expanded p -> expanded (tPrim p)
 | expanded_tBox : expanded tBox.
 
 End expanded.

erasure/theories/EEtaExpandedFix.v

@@ -60,7 +60,7 @@ Inductive expanded (Γ : list nat): term -> Prop :=
     #|args| >= ind_npars mind + cdecl.(cstr_nargs) ->
     Forall (expanded Γ) args ->
     expanded Γ (mkApps (tConstruct ind idx []) args)
-| expanded_tPrim p : primProp (expanded Γ) p -> expanded Γ (tPrim p)
+| expanded_tPrim p : primProp@{Set Set} (expanded Γ) p -> expanded Γ (tPrim p)
 | expanded_tBox : expanded Γ tBox.
 
 End expanded.

erasure/theories/ESubstitution.v

@@ -110,13 +110,13 @@ Proof.
   - econstructor.
     eapply All2_All_mix_left in X3; eauto.
     eapply All2_impl. exact X3.
-    intros ? ? [(? & _) [? []]]; tea.
-    split; eauto.
+    intros ? ? [? [? []]]; tea.
+    split; eauto. eapply o; eauto.
   - econstructor.
     eapply All2_All_mix_left in X3; eauto.
     eapply All2_impl. exact X3.
-    intros ? ? [(? & _) [? []]]; tea.
-    split; eauto.
+    intros ? ? [? [? []]]; tea.
+    repeat split; eauto. now eapply o.
   - econstructor.
     induction H3; constructor.
     induction X2; constructor; depelim X1; eauto.

erasure/theories/Typed/OptimizeCorrectness.v

@@ -3874,6 +3874,8 @@ Section dearg.
 
 End dearg.
 
+Set SsrRewrite.
+
 Lemma env_closed_dearg Σ :
   env_closed (trans_env Σ) ->
   env_closed (trans_env (dearg_env Σ)).

pcuic/theories/Conversion/PCUICNamelessConv.v

@@ -159,15 +159,15 @@ Proof.
     * rewrite forallb_map.
       eapply All_forallb. unfold ondecl in *. solve_all.
       rewrite /nameless_decl /= b.
-      destruct (decl_body x); simpl in *; auto.
+      destruct (decl_body x); simpl in *; auto with bool.
     * induction l.
       + reflexivity.
       + cbn. depelim X0. destruct p0.
         repeat (eapply andb_true_intro ; split) ; try assumption.
         ++ rewrite forallb_map.
            eapply All_forallb. unfold ondecl in *; solve_all.
            rewrite /nameless_decl /= b.
-          destruct (decl_body x); simpl in *; auto.
+          destruct (decl_body x); simpl in *; auto with bool.
         ++ eapply IHl. assumption.
   - simpl ; repeat (eapply andb_true_intro ; split) ; try assumption.
     + induction m.

pcuic/theories/PCUICExpandLetsCorrectness.v

@@ -18,7 +18,7 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICOnOne PCUICCases P
      PCUICCases PCUICWellScopedCumulativity PCUICSpine PCUICSR
      PCUICSafeLemmata PCUICInductives PCUICInductiveInversion.
 From MetaCoq.PCUIC Require Import PCUICExpandLets.
-Set Warnings "+notation_overridden".
+Set Warnings "+notation-overridden".
 
 Import MCMonadNotation.
 

pcuic/theories/PCUICNormal.v

@@ -317,7 +317,7 @@ Proof.
   - inv whn; solve_discr; easy.
 Qed.
 
-Set Firstorder Solver auto with core.
+#[local] Set Firstorder Solver auto with core.
 
 Definition whnf_whne_dec flags Σ Γ t :
   ({∥whnf flags Σ Γ t∥} + {~∥whnf flags Σ  Γ t∥}) *

pcuic/theories/PCUICWcbvEval.v

@@ -837,7 +837,6 @@ Section Wcbv.
     move=> /= Hf Heq'; noconf Heq'.
     eapply closedn_subst0. unfold fix_subst. clear -Hf. generalize #|mfix|.
     induction n; simpl; auto.
-    apply/andP; split; auto.
     simpl. rewrite fix_subst_length. solve_all.
     eapply All_nth_error in Hf; eauto. unfold test_def in Hf.
     rewrite PeanoNat.Nat.add_0_r in Hf. now move/andP: Hf.
@@ -937,8 +936,7 @@ Section Wcbv.
     move=> /= Hf Heq'; noconf Heq'.
     eapply closedn_subst0. unfold cofix_subst. clear -Hf. generalize #|mfix|.
     induction n; simpl; auto.
-    apply/andP; split; auto.
-    simpl. rewrite cofix_subst_length. solve_all.
+    rewrite cofix_subst_length. solve_all.
     eapply All_nth_error in Hf; eauto. unfold test_def in Hf.
     rewrite PeanoNat.Nat.add_0_r in Hf. now move/andP: Hf.
     discriminate.

pcuic/theories/Typing/PCUICClosedTyp.v

@@ -754,7 +754,6 @@ Proof.
   - move: h4; rewrite !on_free_vars_mkApps.
     move=> /andP [] hcofix ->.
     eapply on_free_vars_unfold_cofix in hcofix; eauto.
-    now rewrite hcofix.
   - move: hav; rewrite !on_free_vars_mkApps => /andP [] hcofix ->.
     eapply on_free_vars_unfold_cofix in H as ->; eauto.
   - eapply closed_on_free_vars. rewrite closedn_subst_instance.

template-coq/src/ast_quoter.ml

@@ -100,6 +100,7 @@ struct
   | Sorts.SProp -> Universes0.Sort.Coq_sSProp
   | Sorts.Prop -> Universes0.Sort.Coq_sProp
   | Sorts.Type u -> Universes0.Sort.Coq_sType (quote_universe u)
+  | Sorts.QSort (_, u) -> Universes0.Sort.Coq_sType (quote_universe u) (* FIXME *)
 
   let quote_sort_family s =
     match s with

template-coq/src/constr_quoter.ml

@@ -139,7 +139,7 @@ struct
       | _ -> failwith "byte_ind : tByte is not bound to an inductive type")
 
   let quote_char i =
-    Constr.mkConstruct (Lazy.force byte_ind, (i+1))
+    Constr.UnsafeMonomorphic.mkConstruct (Lazy.force byte_ind, (i+1))
 
   let chars = lazy (Array.init 255 quote_char)
 
@@ -333,6 +333,7 @@ struct
   | Sorts.Prop -> Lazy.force prop
   | Sorts.SProp -> Lazy.force sprop
   | Sorts.Type u -> constr_mkApp (sType, [| Lazy.force tuniverse; quote_universe u |])
+  | Sorts.QSort (_, u) -> constr_mkApp (sType, [| Lazy.force tuniverse; quote_universe u |]) (* FIXME *)
 
   let quote_sort_family = function
     | Sorts.InProp -> Lazy.force sfProp

utils/theories/MCList.v

@@ -1443,7 +1443,6 @@ Lemma forallb_repeat {A} {p : A -> bool} {a : A} {n} :
 Proof.
   intros pa.
   induction n; cbn; auto.
-  now rewrite pa IHn.
 Qed.
 
 Lemma map_repeat {A B} (f : A -> B) a n :

utils/theories/MCPrelude.v

@@ -114,6 +114,11 @@ Hint Extern 10 (@eq nat _ _) => lia : terms.
 
 Ltac easy ::= easy0 || solve [intuition eauto 3 with core terms].
 
+From Coq Require btauto.Algebra.
+
+#[global]
+Hint Extern 5 => progress Algebra.bool : core.
+
 Ltac inv H := inversion_clear H.
 
 (** Turns a subterm of the goal into an evar + equality subgoal

utils/theories/wGraph.v

@@ -656,10 +656,6 @@ Module WeightedGraph (V : UsualOrderedType) (VSet : MSetInterface.S with Module
         apply negb_true_iff in h1. apply VSetFact.not_mem_iff in h1.
         assumption.
     Defined.
-    Next Obligation.
-      apply andb_andI in Hp0 as [? ?]. auto.
-    Defined.
-
 
     Lemma weight_concat {x y z} (p : PathOf x y) (q : PathOf y z)
       : weight (concat p q) = weight p + weight q.
@@ -2219,7 +2215,6 @@ Module WeightedGraph (V : UsualOrderedType) (VSet : MSetInterface.S with Module
       is_simple _ p -> ~~ VSet.mem y (nodes G p) -> is_simple _ (PathOf_add_end p e).
     Proof using HI.
       induction p; simpl; auto.
-      now rewrite andb_true_r.
       move/andP => [nmen iss].
       specialize (IHp e iss). intros Hm%negbe.
       rewrite andb_and. split; auto.