Goal:
    P : Type  b : bool  H : P -> b  X : b -> P
  ============================
   (reflectT P b)


DEBUG:Going to execute:
destruct b

Goals:
    P : Type  H : P -> true  X : true -> P
  ============================
   (reflectT P true)

    P : Type  H : P -> false  X : false -> P
  ============================
   (reflectT P false)


DEBUG:Going to execute:
constructor
DEBUG LTAC Evaluated term: b

Goals:
    P : Type  H : P -> true  X : true -> P
  ============================
   (reflectT P true)

    P : Type  H : P -> false  X : false -> P
  ============================
   (reflectT P false)


DEBUG:Going to execute:
<coq-core.plugins.ltac::constructor@0>

Goals:
    P : Type  H : P -> true  X : true -> P
  ============================
   P

    P : Type  H : P -> false  X : false -> P
  ============================
   (P -> False)


DEBUG:Going to execute:
auto

Goals:
    P : Type  H : P -> true  X : true -> P
  ============================
   P

    P : Type  H : P -> false  X : false -> P
  ============================
   (P -> False)


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3