From 07c5da301d6e770a56214ba2e20fc8714a421485 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 14 Apr 2026 09:32:38 +0200 Subject: [PATCH] Adapt to https://github.com/rocq-prover/stdlib/pull/251 --- theories/lra.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/lra.v b/theories/lra.v index cebe20f..efaceb9 100644 --- a/theories/lra.v +++ b/theories/lra.v @@ -401,10 +401,10 @@ Definition seq_Psatz_Q2Z : seq (Psatz Q) -> seq (Psatz Z) := (* Main tactics, called from the elpi parser (c.f., lra.elpi) *) -Ltac lra_witness n f := let w := fresh "__wit" in wlra_Q w f. -Ltac nra_witness n f := let w := fresh "__wit" in wnra_Q w f. +Ltac lra_witness n f := let w := fresh "__wit" in mp_wlra_Q w f. +Ltac nra_witness n f := let w := fresh "__wit" in mp_wnra_Q w f. Ltac psatz_witness n f := - let w := fresh "__wit" in wsos_Q w f || wpsatz_Q n w f. + let w := fresh "__wit" in mp_wsos_Q w f || mp_wpsatz_Q n w f. Ltac tacF F hyps rff ff varmap wit := let irff := fresh "__rff" in