Commit c6c5de47 authored by Robbert Krebbers's avatar Robbert Krebbers

Try to fix compilation with Coq 8.7.*.

parent fa61a3c0
...@@ -101,7 +101,7 @@ Ltac iFresh := ...@@ -101,7 +101,7 @@ Ltac iFresh :=
side-effect (i.e. to bump the counter) and to return a value (the fresh name). side-effect (i.e. to bump the counter) and to return a value (the fresh name).
We do this by wrapped the side-effect under a [match] in a let-binding. See We do this by wrapped the side-effect under a [match] in a let-binding. See
https://stackoverflow.com/a/46178884 *) https://stackoverflow.com/a/46178884 *)
let _ := let start :=
lazymatch goal with lazymatch goal with
| _ => iStartProof | _ => iStartProof
end in end in
...@@ -109,7 +109,7 @@ Ltac iFresh := ...@@ -109,7 +109,7 @@ Ltac iFresh :=
lazymatch goal with lazymatch goal with
| |- envs_entails (Envs _ _ ?c) _ => c | |- envs_entails (Envs _ _ ?c) _ => c
end in end in
let _ := let inc :=
lazymatch goal with lazymatch goal with
| |- envs_entails (Envs ?Δp ?Δs _) ?Q => | |- envs_entails (Envs ?Δp ?Δs _) ?Q =>
let c' := eval vm_compute in (Pos.succ c) in let c' := eval vm_compute in (Pos.succ c) in
......
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