The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I have the following goal in Coq 8.4pl6 (after Grab Existential Variables; it is left over because I did an [exact_no_check]):

2 subgoals, subgoal 1 (ID 15945)
 
  Char : Type
  HSL : StringLike Char
  HSLP : StringLikeProperties Char
  ls : list (string * productions Char)
  data : boolean_parser_dataT
  constT : Type
  varT : Type
  strC : str_carrier constT varT
  str : String
  nt : string
  a : nat * nat
  x : forall x : nat * nat,
      prod_relation lt lt x a ->
      nonterminals_listT ->
      varT -> forall x2 : nat, x2 <= fst x -> string -> bool
  y : forall x0 : nat * nat,
      prod_relation lt lt x0 a ->
      nonterminals_listT ->
      varT -> forall x3 : nat, x3 <= fst x0 -> string -> bool
  H : forall_relation
        (fun a' : nat * nat =>
         pointwise_relation (prod_relation lt lt a' a)
           (forall_relation
              (fun _ : nonterminals_listT =>
               forall_relation
                 (fun _ : varT =>
                  forall_relation
                    (fun d : nat =>
                     forall_relation
                       (fun _ : d <= fst a' =>
                        forall_relation (fun _ : string => eq))))))) x y
  a0 : nonterminals_listT
  a1 : varT
  a2 : nat
  a3 : a2 <= fst a
  a4 : string
  b : ~ a2 < fst a
  a5 : (negb (EqNat.beq_nat (snd a) 0) && is_valid_nonterminal a0 a4)%bool =
       true
  ============================
   forall x0 : nat * nat,
   prod_relation lt lt x0 a ->
   nonterminals_listT ->
   varT -> forall x3 : nat, x3 <= fst x0 -> string -> bool

subgoal 2 (ID 15869) is:
 forall x0 : nat * nat,
 prod_relation lt lt x0 a ->
 nonterminals_listT ->
 varT -> forall x3 : nat, x3 <= fst x0 -> string -> bool

(dependent evars: ?15719 using ?15743 , ?15743 using ?15776 ?15775 ?15774 , ?15774 using ?15964 , ?15775 using , ?15776 using ?15809 ?15808 , ?15808 using ?15834 , ?15809 using ?15885 ?15884 , ?15834 using ?15864 , ?15864 using ?15869 , ?15865 using , ?15869 open, ?15884 using ?15910 , ?15885 using , ?15910 using ?15940 , ?15940 using ?15945 , ?15945 open, ?15964 using ?16010 ?16009 ?16008 ?16007 , ?16007 using , ?16008 using ?16064 ?16063 ?16062 , ?16009 using ?16038 ?16036 , ?16010 using , ?16035 using , ?16036 using ?16048 ?16046 , ?16037 using , ?16038 using , ?16045 using , ?16046 using , ?16047 using , ?16048 using , ?16062 using ?16144 ?16143 , ?16063 using , ?16064 using ?16132 ?16130 , ?16129 using , ?16130 using , ?16131 using , ?16132 using , ?16143 using , ?16144 using ,)

I try [exact y], and it fails, telling me that y cannot be found in the current environment.  Yet [y] appears.  I have done C-c C-p to refresh the goal, and nothing changes.  I run the following tactic to list the hypotheses:
    try match goal with
          | [ H : _ |- _ ] => idtac H; fail
        end.

and get the list:
a5
b
a4
a3
a2
a1
a0
x
a
nt
str
strC
varT
constT
data
ls
HSLP
HSL
Char

What might be going on here?

-Jason