Skip to content
  • Robbert Krebbers's avatar
    Make reflexivity hints work for evars. · e2458a73
    Robbert Krebbers authored
    Since Coq 8.4 did not backtrack on eauto premises, we used to ensure
    that hints like
      Hint Extern 0 (?x ≡{_}≡ ?y) => reflexivity.
    were not used for goals involving evars by writing ?x ≡{_}≡ ?y instead
    of _ ≡{_}≡ _.
    This seems to be a legacy issue that no longer applies to Coq 8.5, so
    I have removed these restrictions making these hints thus more powerful.