theories/proofmode · 4d6d497af5e4ba4d5a432efdb7f3b9708f2ae3af · Gaëtan Gilbert / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

3710 commits behind the upstream repository.

Explicitly use core hint database

Tej Chajed authored 6 years ago

Adding a hint without a database now triggers a deprecation warning in
Coq master (https://github.com/coq/coq/pull/8987).

4d6d497a

4d6d497a 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