search

FissoreD / coq-elpi

Coq plugin embedding elpi
GNU Lesser General Public License v2.1
0 stars 0 forks source link

Subgoals are put into the shelf #18

Closed FissoreD closed 2 weeks ago

FissoreD commented 2 weeks ago 
From elpi.apps Require Import tc.
Class A (n : nat).
Class B.

Instance a : A 0 := {}.

Lemma foo: forall x `{A x}, True -> B. Admitted.

Goal B.
  refine (foo _  _).
  (* Note: the subgoal True is put into the shelf, however, we expect it to be in the list of goal to treat *)
  Fail auto.
Qed.