Fixing some spurious axioms introduced by tauto/intuition
The axioms are exculded middle and Eq_dep.eq_rect_eq.
Showing
- Core/Formalism.v 8 additions, 10 deletionsCore/Formalism.v
- Gathering/InR2/Algorithm.v 4 additions, 4 deletionsGathering/InR2/Algorithm.v
- Gathering/InR2/FSyncFlexNoMultAlgorithm.v 4 additions, 2 deletionsGathering/InR2/FSyncFlexNoMultAlgorithm.v
- Spectra/SetSpectrum.v 6 additions, 2 deletionsSpectra/SetSpectrum.v
Loading
Please register or sign in to comment