theories/proofmode · 1ad44fff3970c45e0615dc897960e6c4463b2cf3 · Michael Sammler / iris-coq · GitLab

Snippets Groups Projects

Forked from Iris / Iris

3228 commits behind the upstream repository.

Have `iNext` turn `Next x ≡ Next y` into `x ≡ y`.

Robbert Krebbers authored 5 years ago

ee8815c0

ee8815c0 5 years ago

Name	Last commit	Last update
..
base.v
class_instances_bi.v
class_instances_sbi.v
classes.v
coq_tactics.v
environments.v
frame_instances.v
intro_patterns.v
ltac_tactics.v
modalities.v
modality_instances.v
monpred.v
notation.v
reduction.v
sel_patterns.v
spec_patterns.v
tactics.v
tokens.v