Commit fa61a3c0 authored by Robbert Krebbers's avatar Robbert Krebbers

Update documentation of [iFresh] and make sure it returns the old counter.

parent 8d24e722
......@@ -91,25 +91,31 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
end.
(** * Generate a fresh identifier *)
(* Tactic Notation tactics cannot return terms *)
(** The tactic [iFresh] bumps the fresh name counter in the proof mode
environment and returns the old value.
Note that we use [Ltac] instead of [Tactic Notation] since [Tactic Notation]
tactics can only have side-effects, but cannot return terms. *)
Ltac iFresh :=
(* We need to increment the environment counter using [tac_fresh].
But because [iFresh] returns a value, we have to let bind
[tac_fresh] wrapped under a match to force evaluation of this
side-effect. See https://stackoverflow.com/a/46178884 *)
let do_incr :=
(* We make use of an Ltac hack to allow the [iFresh] tactic to both have a
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
https://stackoverflow.com/a/46178884 *)
let _ :=
lazymatch goal with
| _ =>
iStartProof;
lazymatch goal with
| |- envs_entails (Envs ?Δp ?Δs ?c) ?Q =>
let c' := eval vm_compute in (Pos.succ c) in
convert_concl_no_check (envs_entails (Envs Δp Δs c') Q)
end
| _ => iStartProof
end in
lazymatch goal with
|- envs_entails (Envs _ _ ?c) _ => constr:(IAnon c)
end.
let c :=
lazymatch goal with
| |- envs_entails (Envs _ _ ?c) _ => c
end in
let _ :=
lazymatch goal with
| |- envs_entails (Envs ?Δp ?Δs _) ?Q =>
let c' := eval vm_compute in (Pos.succ c) in
convert_concl_no_check (envs_entails (Envs Δp Δs c') Q)
end in
constr:(IAnon c).
(** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
......
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