Skip to content
GitLab
Switch branch/tag
Find file Normal viewHistoryPermalink
base.v 232 Bytes
Newer Older
Ralf Jung's avatar
turns out we can import with shorter names (and we actually already do that...    
Ralf Jung committed
1 
From mathcomp Require Export ssreflect.
Robbert Krebbers's avatar
Give the project a top-level name so it can be make installed.    
Robbert Krebbers committed
2 
From iris.prelude Require Export prelude.
Ralf Jung's avatar
more restrictive Proof Using hints in base_logic, algebra    
Ralf Jung committed
3 
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Use ssreflect for modures.  
Robbert Krebbers committed
4 
Global Set Bullet Behavior "Strict Subproofs".
Robbert Krebbers's avatar
Use new Import/Export syntax everywhere.    
Robbert Krebbers committed
5 
Global Open Scope general_if_scope.
Ralf Jung's avatar
make "make quick" quick by adding hints about the used section variables    
Ralf Jung committed
6 
Ltac done := prelude.tactics.done.