Update apps/tc/README.md

[gares]

TODO/questions:

• #[name="name",graft(before="this")] TC.Instance foo that add/replaces foo.
• TC.Declare should set modes to input by default
• TC.Declare should declare "class methods" so that this works

   Class Eqb (T: Type) := {
      eqb : T -> T -> bool; 
      eqb_leibniz A B: eqb A B = true <-> A = B
  }.
  #[refine] Instance eqBool : Eqb bool := {
    eqb x y := if x then y else negb y
  }.
  Proof. intros [] []; intuition. Qed.
  

• TC.unfold constant.
• TC.failsafe class adds a rule for class that makes it fail safe, unresolved goals are given back to the user and displayed by Coq (requires @no-tc!) from @Tragicus
• use the bool parameter named fail in the .ml code and assert the list of new/shelved goals is empty
• order of impargs in TC.Declare
• subclasses events wrong order
• don't call partition before msolve, expose partition/clusterize as an API on goals.
• msolve and solve are both called in case of a failre (remove rules for solve)

[FissoreD]

TC.Declare should declare "class methods" so that this works

In pure coq, we get the same error of unbound method name:

Record Eqb (T: Type) := {
    eqb : T -> T -> bool; 
    eqb_leibniz A B: eqb A B = true <-> A = B
}.

Existing Class Eqb.

#[refine] Instance eqBool : Eqb bool := {
  eqb x y := if x then y else negb y
}.
Proof. intros [] []; intuition. Qed.

the call to Record.declare_existing_class does not build the class mehods.