Skip to content

GitLab

I
Iris
Commit 2eb91537 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Fix bug reference.

parent cf4effe5
Hide whitespace changes
Inline Side-by-side
Showing with 1 addition and 1 deletion
theories/proofmode/tactics.v
View file @ 2eb91537
...@@ -390,7 +390,7 @@ resolved at arbitrary moments. It seems that tactics like `apply`, `split` and ...@@ -390,7 +390,7 @@ resolved at arbitrary moments. It seems that tactics like `apply`, `split` and
triggered too eagerly, this tactic uses `refine` at various places instead of triggered too eagerly, this tactic uses `refine` at various places instead of
`apply`. `apply`.
TODO: Investigate what really is going on. Is there a related to Cog bug #5752? TODO: Investigate what really is going on. Is there a related to Cog bug #4969?
When should holes in an `open_constr` be resolved? When should holes in an `open_constr` be resolved?
*) *)
Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) := Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
......
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