Files

 master

/

lib

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

bschommer

and

xavierleroy

Add some 64-bit operations and properties

Feb 4, 2025

f1df1a1 · Feb 4, 2025

History

History

/

lib

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
Axioms.v		Axioms.v	Use the LGPL instead of the GPL for dual-licensed files	May 8, 2021
BoolEqual.v		BoolEqual.v	Extend the boolean_equality tactic (#429)	Jun 25, 2022
Camlcoq.ml		Camlcoq.ml	Use the LGPL instead of the GPL for dual-licensed files	May 8, 2021
Commandline.ml		Commandline.ml	Add Commandline.longopt function for options of the form `-<key>=<a…	Sep 23, 2022
Commandline.mli		Commandline.mli	Add Commandline.longopt function for options of the form `-<key>=<a…	Sep 23, 2022
Coqlib.v		Coqlib.v	Some properties about two_p, mulhu and mulhs.	Sep 3, 2024
Decidableplus.v		Decidableplus.v	Qualify Instance and Program Instance as Global	Oct 3, 2021
FSetAVLplus.v		FSetAVLplus.v	Use the LGPL instead of the GPL for dual-licensed files	May 8, 2021
Floats.v		Floats.v	Avoid relying on intuition being intuition auto with * (#496)	Jul 10, 2023
Heaps.v		Heaps.v	Use the LGPL instead of the GPL for dual-licensed files	May 8, 2021
IEEE754_extra.v		IEEE754_extra.v	Adapt to rocq-prover/rocq#19801 (#535)	Jan 9, 2025
Integers.v		Integers.v	Add some 64-bit operations and properties	Feb 4, 2025
Intv.v		Intv.v	Avoid relying on intuition being intuition auto with * (#496)	Jul 10, 2023
IntvSets.v		IntvSets.v	Avoid relying on intuition being intuition auto with * (#496)	Jul 10, 2023
Iteration.v		Iteration.v	Address most deprecation warnings from Coq 8.16	Mar 10, 2023
Lattice.v		Lattice.v	An improved PTree data structure (#420)	Nov 16, 2021
Maps.v		Maps.v	Address Coq 8.18 warnings	Mar 19, 2024
Ordered.v		Ordered.v	Use the LGPL instead of the GPL for dual-licensed files	May 8, 2021
Parmov.v		Parmov.v	Address Coq 8.18 warnings	Mar 19, 2024
Postorder.v		Postorder.v	Use the LGPL instead of the GPL for dual-licensed files	May 8, 2021
Printlines.ml		Printlines.ml	Replace CR, FF and VT with whitespace.	Nov 5, 2022
Printlines.mli		Printlines.mli	Use the LGPL instead of the GPL for dual-licensed files	May 8, 2021
Readconfig.mli		Readconfig.mli	Use the LGPL instead of the GPL for dual-licensed files	May 8, 2021
Readconfig.mll		Readconfig.mll	Use the LGPL instead of the GPL for dual-licensed files	May 8, 2021
Responsefile.mli		Responsefile.mli	Use the LGPL instead of the GPL for dual-licensed files	May 8, 2021
Responsefile.mll		Responsefile.mll	Use the LGPL instead of the GPL for dual-licensed files	May 8, 2021
Tokenize.mli		Tokenize.mli	Use the LGPL instead of the GPL for dual-licensed files	May 8, 2021
Tokenize.mll		Tokenize.mll	Use the LGPL instead of the GPL for dual-licensed files	May 8, 2021
UnionFind.v		UnionFind.v	Avoid Global Set Asymmetric Patterns (#408)	Sep 15, 2021
Wfsimpl.v		Wfsimpl.v	Use the LGPL instead of the GPL for dual-licensed files	May 8, 2021
Zbits.v		Zbits.v	Improve value analysis for divu and divs	Sep 9, 2024
View all files