Commit 45fd520d authored by Ralf Jung's avatar Ralf Jung
Browse files

avoid section variables for real

parent c4055887
Pipeline #67839 passed with stage
in 4 minutes and 38 seconds
...@@ -12,7 +12,7 @@ Proof. naive_solver. Qed. ...@@ -12,7 +12,7 @@ Proof. naive_solver. Qed.
Section map_notations. Section map_notations.
(* Avoiding section variables so output is not affected by (* Avoiding section variables so output is not affected by
https://github.com/coq/coq/pull/16208 *) https://github.com/coq/coq/pull/16208 *)
Let M := gmap nat. Notation M := (gmap nat).
Definition test_2 : M (M nat) := {[ 10 := {[ 10 := 1 ]}; 20 := {[ 20 := 2]} ]}. Definition test_2 : M (M nat) := {[ 10 := {[ 10 := 1 ]}; 20 := {[ 20 := 2]} ]}.
Definition test_3 : 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