Skip to content
Snippets Groups Projects
Normal view Permalink
base.v 223 B
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.
Ralf Jung's avatar
use coq-stdpp  
Ralf Jung committed
2 
From stdpp 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
use coq-stdpp  
Ralf Jung committed
6 
Ltac done := stdpp.tactics.done.