Anomaly when admitting obligations

[TDiazT]

trafficstars

Hi, I was trying to define a function and tried to admit the obligation and got a Error: Anomaly "Uncaught exception Environ.NotEvaluableConst(0)." Please report at http://coq.inria.fr/bugs/..

I noticed there was a similar issue from before which was fixed, so I am not sure if it's the same really...

I am working with Equations 1.2beta and Ssreflect. Here is an example code:

From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


From Equations Require Import Equations.



Section Test.

  Variables Name : eqType.

   Inductive Query : Type :=
  | SingleField : Name -> nat -> Query
  | LabeledField : Name -> Name -> nat -> Query
  | NestedField : Name -> nat -> seq Query -> Query
  | NestedLabeledField : Name -> Name -> nat -> seq Query -> Query
  | InlineFragment : Name -> seq Query -> Query.


   

  Equations get_subqueries : seq (option Query) -> seq Query :=
    {
      get_subqueries [::] := [::];
      get_subqueries ((Some q) :: tl) := q :: get_subqueries tl;
      get_subqueries (None :: tl) := get_subqueries tl
    }.
  
  Equations query_of_tree (tree : GenTree.tree (option Name * Name * nat)) : option Query :=
    {
      query_of_tree (GenTree.Node 0 [:: GenTree.Leaf  (None, f, α)]) := Some (SingleField f α);
      query_of_tree (GenTree.Node 1 [:: GenTree.Leaf (Some l, f, α)]) := Some (LabeledField l f α);
      query_of_tree (GenTree.Node 2  (GenTree.Leaf (None, f, α) :: subtree)) :=
        Some (NestedField f α (get_subqueries [seq (query_of_tree t) | t <- subtree]));
      
      query_of_tree (GenTree.Node 3  (GenTree.Leaf (Some l, f, α) :: subtree)) :=
          Some (NestedLabeledField l f α (get_subqueries [seq (query_of_tree t) | t <- subtree]));
      
      query_of_tree (GenTree.Node 4  (GenTree.Leaf (None, t, emptym) :: subtree)) :=
        Some (InlineFragment t (get_subqueries [seq (query_of_tree t) | t <- subtree]));
         

      query_of_tree _ := None

    }.
   Admit Obligations.

End Test.

On another note but related, why is it asking to prove query_of_tree_graph tree (query_of_tree tree) ? It can't generate the graph?