From d9cb7fc06952bc2be0664d540aab7d174d8f16a2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 4 May 2026 15:13:56 +0200 Subject: [PATCH] Adapt to rocq-prover/rocq#21987 (clear checks that ids are bound even when from match goal) --- driver/Compiler.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/driver/Compiler.v b/driver/Compiler.v index 44791ac8f..5535e84e8 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -361,7 +361,7 @@ Ltac DestructM := match goal with [ H: exists p, _ /\ _ |- _ ] => let p := fresh "p" in let M := fresh "M" in let MM := fresh "MM" in - destruct H as (p & M & MM); clear H + destruct H as (p & M & MM); try clear H end. repeat DestructM. subst tp. assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p21)).