Fourier.v « micromega « plugins - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/plugins/micromega/Fourier.v

blob: 0153de1dabdde48b1722cf998ebd8c4cc7630bf7 (plain)

Require Import Lra.
Require Export Fourier_util.

#[deprecated(since = "8.9.0", note = "Use lra instead.")]
Ltac fourier := lra.