adapt to coq/coq#18729

andres-erbsen · Mar 2, 2024 · e5fe91b · e5fe91b
1 parent 06509a9
commit e5fe91b
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 4 deletions.
diff --git a/theories/Torch/Tensor.v b/theories/Torch/Tensor.v
@@ -583,7 +583,7 @@ Module RawIndex.
     end.
     specialize (IHr ltac:(Z.to_euclidean_division_equations; nia)).
     destruct IHr as [IHr1 IHr2].
-    rewrite IHr1; repeat split; try (now destruct r); try lia; [].
+    rewrite IHr1; repeat split; try (now destruct r); try lia;
     Z.to_euclidean_division_equations; nia.
   Qed.
 
@@ -1335,5 +1335,3 @@ Definition coer_tensor {r s A B} {coerAB : has_coer A B} : @tensor r s A -> @ten
 #[export] Set Warnings Append "-uniform-inheritance,-ambiguous-paths".
 #[local] Set Warnings Append "-unsupported-attributes".
 #[export] Coercion coer_tensor : tensor >-> tensor.
-#[local] Set Warnings Append "unsupported-attributes".
-#[export] Set Warnings Append "uniform-inheritance,ambiguous-paths".
diff --git a/theories/Util/Wf_Uint63.v b/theories/Util/Wf_Uint63.v
@@ -94,7 +94,7 @@ Proof.
                 else state)
             i
             init).
-  { abstract
+  { clear dependent A; abstract
       (cbv [is_true];
        pose proof (Uint63.to_Z_bounded max);
        pose proof (Uint63.to_Z_bounded i);