Commit 33272af5 authored by Hugo Herbelin's avatar Hugo Herbelin

Adapting to Coq PR#10832: formats associated to a given interpretation

of a notation are now taken into account (fixing Coq issue #6082).

Here, the format associated to the notation ";;" in
theories/heap_lang/notation.v is now taken into account.
parent 60647cc2
......@@ -28,6 +28,6 @@
| InjR "l" =>
let: "tmp1" := Fst ! "l" in
let: "tmp2" := Snd ! "l" in
"l" <- ("tmp1", acc);; rev "tmp2" (InjLV #())
"l" <- ("tmp1", acc) ;; rev "tmp2" (InjLV #())
end [{ v, Φ v }]
Markdown is supported
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