theories/proofmode · 0e078666b4c97c1847172a9c4320807fe3493170 · Gaëtan Gilbert / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

3669 commits behind the upstream repository.

A bit of refactoring of the `iIntro` tactics.

Robbert Krebbers authored 6 years ago

- More consistent indentation.
- Mark new subgoals as comments.

0e078666

0e078666 6 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