diff --git a/test-normalizer.sed b/test-normalizer.sed index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..97b8c63c2eee5611528c8145d278bb2de7ebebfc 100644 --- a/test-normalizer.sed +++ b/test-normalizer.sed @@ -0,0 +1,2 @@ +# adjust for https://github.com/coq/coq/pull/13656 +s/subgoal/goal/g diff --git a/tests/telescopes.ref b/tests/telescopes.ref index 485cc5c18c71d09f2ab7c5b483af8515019faf5a..afac10f0b0fddd77cc435c1097c467da2a88d1fb 100644 --- a/tests/telescopes.ref +++ b/tests/telescopes.ref @@ -1,16 +1,16 @@ -1 subgoal +1 goal X : tele α, β, γ1, γ2 : X → Prop ============================ accessor α β γ1 → accessor α β (λ.. x : X, γ1 x ∨ γ2 x) -1 subgoal +1 goal X : tele α, β, γ1, γ2 : X → Prop ============================ ∀.. x : X, γ1 x → (λ.. x0 : X, γ1 x0 ∨ γ2 x0) x -1 subgoal +1 goal X : tele α, β, γ1, γ2 : X → Prop