From 8d9596029b1ee936255939de7904a58083d9af3c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 21 Sep 2020 15:51:24 +0200 Subject: [PATCH] Fix after merge --- pcuic/theories/PCUICInductiveInversion.v | 2 +- pcuic/theories/PCUICSpine.v | 4 ++-- safechecker/theories/PCUICSafeChecker.v | 4 ---- 3 files changed, 3 insertions(+), 7 deletions(-) diff --git a/pcuic/theories/PCUICInductiveInversion.v b/pcuic/theories/PCUICInductiveInversion.v index 6ab3b6f18..fe983f383 100644 --- a/pcuic/theories/PCUICInductiveInversion.v +++ b/pcuic/theories/PCUICInductiveInversion.v @@ -2643,7 +2643,7 @@ Proof. exists x; intuition eauto. now rewrite ConstraintSetFact.add_iff. firstorder eauto. - subst. exists x0; firstorder. + subst. exists x0; firstorder auto with *. Qed. Lemma subst_instance_variance_cstrs l u i i' : diff --git a/pcuic/theories/PCUICSpine.v b/pcuic/theories/PCUICSpine.v index dfa139adf..3668e7624 100644 --- a/pcuic/theories/PCUICSpine.v +++ b/pcuic/theories/PCUICSpine.v @@ -856,11 +856,11 @@ Proof. rewrite Nat.add_0_r. specialize (X (subst_context (skipn #|Γ0| s) 0 Γ0) ltac:(now autorewrite with len) _ _ (subst [t1] #|Γ0| T) cs subsl'). - rewrite -{1}H0. apply X. + rewrite -{1}H1. apply X. rewrite -subst_app_simpl'. apply subslet_length in subsl'. now autorewrite with len in subsl'. - rewrite -H0. now rewrite firstn_skipn. + rewrite -H1. now rewrite firstn_skipn. Qed. Lemma arity_spine_it_mkProd_or_LetIn_Sort {cf:checker_flags} Σ Γ ctx s args inst : diff --git a/safechecker/theories/PCUICSafeChecker.v b/safechecker/theories/PCUICSafeChecker.v index 7d979abdb..cd07618ca 100644 --- a/safechecker/theories/PCUICSafeChecker.v +++ b/safechecker/theories/PCUICSafeChecker.v @@ -100,14 +100,10 @@ Proof. now rewrite IHt1. Qed. -Derive NoConfusion for sort_family. -Derive EqDec for sort_family. - Definition mkApps_decompose_app t : t = mkApps (fst (decompose_app t)) (snd (decompose_app t)) := mkApps_decompose_app_rec t []. - Derive NoConfusion EqDec for sort_family. Inductive type_error :=