diff --git a/test-normalizer.sed b/test-normalizer.sed index e41a342535ef38ec32e9dde0e561f84ac1b69065..3f9662bba47b73b0deac50eb948f084345fc0404 100644 --- a/test-normalizer.sed +++ b/test-normalizer.sed @@ -4,3 +4,5 @@ s/subgoal/goal/g /[0-9]* focused goals\?$/{N;s/\n */ /;} # locations in Fail added in https://github.com/coq/coq/pull/15174 /^File/d +# extra space removed in https://github.com/coq/coq/pull/16130 +s/= $/=/ diff --git a/tests/notation.ref b/tests/notation.ref index 4d53c67c775137daaf00f3b83ff54b17c83080ef..b5b7abc69f878355a6abc12c887cb6e674bfea87 100644 --- a/tests/notation.ref +++ b/tests/notation.ref @@ -1,21 +1,21 @@ test_2 = {[10 := {[10 := 1]}; 20 := {[20 := 2]}]} : M (M nat) -test_3 = +test_3 = {[10 := {[10 := 1]}; 20 := {[20 := 2]}; 30 := {[30 := 3]}]} : M (M nat) -test_4 = +test_4 = {[10 := {[10 := 1]}; 20 := {[20 := 2]}; 30 := {[30 := 3]}; 40 := {[40 := 4]}]} : M (M nat) -test_op_2 = +test_op_2 = {[10 := {[10 ^ 2 := 99]}; 10 + 1 := {[10 - 100 := 42 * 1337]}]} : M (M nat) -test_op_3 = +test_op_3 = {[10 := {[20 - 2 := [11]; 1 := [22]]}; 20 := {[99 + length [1] := [1; 2; 3]]}; 4 := {[4 := [4]]}; 5 := {[5 := [5]]}]} : M (M (list nat)) -test_op_4 = +test_op_4 = {[10 := {[20 - 2 := [11]; 1 := [22]; 3 := [23]; @@ -30,6 +30,6 @@ test_gmultiset_2 = {[+ 10; 11 +]} : gmultiset nat test_gmultiset_3 = {[+ 10; 11; 2 - 2 +]} : gmultiset nat -test_gmultiset_4 = +test_gmultiset_4 = {[+ {[+ 10 +]}; ∅; {[+ 2 - 2; 10 +]} +]} : gmultiset (gmultiset nat)