"git-rts@gitlab.mpi-sws.org:svancollem/iris.git" did not exist on "e2458a73923c782210e501029aa7cceb7e080f04"
Forked from
Iris / Iris
7437 commits behind the upstream repository.
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.| Name | Last commit | Last update |
|---|---|---|
| algebra | ||
| docs | ||
| heap_lang | ||
| prelude | ||
| program_logic | ||
| .gitignore | ||
| LICENSE | ||
| Makefile | ||
| README | ||
| _CoqProject |