• 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.
    e2458a73
base.v 39.7 KB