Forked from
Iris / Iris
3697 commits behind the upstream repository.
Tej Chajed
authored
Adding a hint without a database now triggers a deprecation warning in Coq master (https://github.com/coq/coq/pull/8987).
| Name | Last commit | Last update |
|---|---|---|
| .. | ||
| lib | ||
| bi.v | ||
| big_op.v | ||
| derived_connectives.v | ||
| derived_laws_bi.v | ||
| derived_laws_sbi.v | ||
| embedding.v | ||
| interface.v | ||
| monpred.v | ||
| notation.v | ||
| plainly.v | ||
| tactics.v | ||
| telescopes.v | ||
| updates.v | ||
| weakestpre.v | ||