Fix after merge

MetaCoq · Sep 21, 2020 · 8d95960 · 8d95960
1 parent 4186c44
commit 8d95960
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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 :=