Commit 48b5fd55 authored by Robbert Krebbers's avatar Robbert Krebbers

Mention Coq issue 6583.

parent 2eb91537
...@@ -383,15 +383,11 @@ Notation "( H $! x1 .. xn 'with' pat )" := ...@@ -383,15 +383,11 @@ Notation "( H $! x1 .. xn 'with' pat )" :=
Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0). Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
(* (*
There is some hacky stuff going on here (most probably there is a Coq bug). There is some hacky stuff going on here: because of Coq bug #6583, unresolved
Holes -- like unresolved type class instances -- in the argument `xs` are type classes in the arguments `xs` are resolved at arbitrary moments. Tactics
resolved at arbitrary moments. It seems that tactics like `apply`, `split` and like `apply`, `split` and `eexists` wrongly trigger type class search to resolve
`eexists` trigger type class search to resolve these holes. To avoid TC being these holes. To avoid TC being triggered too eagerly, this tactic uses `refine`
triggered too eagerly, this tactic uses `refine` at various places instead of at most places instead of `apply`.
`apply`.
TODO: Investigate what really is going on. Is there a related to Cog bug #4969?
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) :=
let rec go xs := let rec go 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