make sure all Instance/Argument have explicit visibility
Showing
- Makefile.coq.local 11 additions, 0 deletionsMakefile.coq.local
- coq-lint.sh 12 additions, 0 deletionscoq-lint.sh
- theories/lang/adequacy.v 1 addition, 1 deletiontheories/lang/adequacy.v
- theories/lang/heap.v 2 additions, 2 deletionstheories/lang/heap.v
- theories/lang/lang.v 12 additions, 12 deletionstheories/lang/lang.v
- theories/lang/lib/arc.v 2 additions, 2 deletionstheories/lang/lib/arc.v
- theories/lang/lib/spawn.v 1 addition, 1 deletiontheories/lang/lib/spawn.v
- theories/lang/lifting.v 6 additions, 6 deletionstheories/lang/lifting.v
- theories/lifetime/lifetime.v 1 addition, 1 deletiontheories/lifetime/lifetime.v
- theories/lifetime/lifetime_sig.v 1 addition, 1 deletiontheories/lifetime/lifetime_sig.v
- theories/lifetime/meta.v 1 addition, 1 deletiontheories/lifetime/meta.v
- theories/lifetime/model/definitions.v 7 additions, 7 deletionstheories/lifetime/model/definitions.v
- theories/lifetime/model/primitive.v 8 additions, 8 deletionstheories/lifetime/model/primitive.v
- theories/typing/function.v 2 additions, 2 deletionstheories/typing/function.v
- theories/typing/lft_contexts.v 8 additions, 8 deletionstheories/typing/lft_contexts.v
- theories/typing/lib/arc.v 1 addition, 1 deletiontheories/typing/lib/arc.v
- theories/typing/lib/brandedvec.v 1 addition, 1 deletiontheories/typing/lib/brandedvec.v
- theories/typing/lib/ghostcell.v 3 additions, 3 deletionstheories/typing/lib/ghostcell.v
- theories/typing/lib/rc/rc.v 1 addition, 1 deletiontheories/typing/lib/rc/rc.v
- theories/typing/lib/refcell/refcell.v 1 addition, 1 deletiontheories/typing/lib/refcell/refcell.v
Loading