Commit c4055887 authored by Ralf Jung's avatar Ralf Jung
Browse files

avoid section variables in printed terms

parent 0a010579
Pipeline #67789 passed with stage
in 6 minutes and 54 seconds
......@@ -6,5 +6,3 @@ s/subgoal/goal/g
/^File/d
# extra space removed in https://github.com/coq/coq/pull/16130
s/= $/=/
# delete "uses section variable" lines (https://github.com/coq/coq/pull/16208)
/^[^ ]+ uses section variables? .*\.$/d
From stdpp Require Import base tactics fin_maps gmultiset.
From stdpp Require Import base tactics fin_maps gmap gmultiset.
(** Test parsing of variants of [(≡)] notation. *)
Lemma test_equiv_annot_sections `{!Equiv A, !Equivalence (@{A})} (x : A) :
......@@ -10,7 +10,9 @@ Proof. naive_solver. Qed.
(** Test that notations for maps with multiple elements can be parsed and printed correctly. *)
Section map_notations.
Context `{FinMap nat M}.
(* Avoiding section variables so output is not affected by
https://github.com/coq/coq/pull/16208 *)
Let M := gmap nat.
Definition test_2 : M (M nat) := {[ 10 := {[ 10 := 1 ]}; 20 := {[ 20 := 2]} ]}.
Definition test_3 : M (M nat) := {[ 10 := {[ 10 := 1 ]}; 20 := {[ 20 := 2]};
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment