From bfbd4eeb7643b10fe1ef994131f977866dc866f7 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 6 Jul 2024 15:00:52 +0200 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19310 --- src/TacticsUtil.v.cppo | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/TacticsUtil.v.cppo b/src/TacticsUtil.v.cppo index 375a5b30..584ebba3 100644 --- a/src/TacticsUtil.v.cppo +++ b/src/TacticsUtil.v.cppo @@ -13,7 +13,11 @@ From Ltac2 Require Import Ltac2. From Ltac2 Require Import Message. From Ltac2 Require Import Constr. +#if COQ_VERSION >= (8, 21, 0) +Ltac2 ltac1_congruence () := Ltac1.run (Ltac1.ref [ident:(Stdlib); ident:(Init); ident:(Prelude); ident:(congruence)]). +#else Ltac2 ltac1_congruence () := Ltac1.run (Ltac1.ref [ident:(Coq); ident:(Init); ident:(Prelude); ident:(congruence)]). +#endif Ltac2 Notation "congruence" := ltac1_congruence (). (* From https://github.com/tchajed/coq-ltac2-experiments/blob/master/src/Ltac2Lib.v *)