Skip to content
  • Jacques-Henri Jourdan's avatar
    Change the tactic for resolving typeclass instances from canonical structures. · 011e9bbb
    Jacques-Henri Jourdan authored
    Example include Equiv, Dist, Op, Core, Valid, ValidN and Unit.
    
    The previous hints used eapply. The new hint now use refine. These two
    tactic use a different unification algorithm, which result in
    different behavior with respect to canonical structures.
    
    The refine tactic is followed by shelving all the remaining goals,
    which correspond actually to existential variables.
    
    In particular, in RustHornBelt, the version using apply is unable to
    find the canonical structure of heterogeneous lists.
    011e9bbb