Collapse file tree

Files

 master

/

lib

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

robbertkrebbers

Remove duplicate Forall2 notions.

Oct 30, 2014

ab9b194 · Oct 30, 2014

History

History

/

lib

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
Axioms.v		Axioms.v	Axioms: remove prop_ext, currently unused AND unsound in Coq 8.4.	Dec 15, 2013
Camlcoq.ml		Camlcoq.ml	Merge of "newspilling" branch:	Jul 23, 2014
Coqlib.v		Coqlib.v	Remove duplicate Forall2 notions.	Oct 30, 2014
FSetAVLplus.v		FSetAVLplus.v	Update LICENSE file and headers for dual-licensed files.	Jun 17, 2013
Fappli_IEEE_extra.v		Fappli_IEEE_extra.v	Upgrade to flocq 2.4.0	Oct 7, 2014
Floats.v		Floats.v	Upgrade to flocq 2.4.0	Oct 7, 2014
Heaps.v		Heaps.v	Assorted cleanups, esp. to avoid generating _rec and _rect recursors in	Mar 9, 2013
Integers.v		Integers.v	Tweaks to support defunctorization.	Jul 23, 2014
Intv.v		Intv.v	Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.	Mar 9, 2011
IntvSets.v		IntvSets.v	Merge of branch value-analysis.	Dec 20, 2013
Iteration.v		Iteration.v	Update LICENSE file and headers for dual-licensed files.	Jun 17, 2013
Lattice.v		Lattice.v	Merge of branch value-analysis.	Dec 20, 2013
Maps.v		Maps.v	Remove duplicate Forall2 notions.	Oct 30, 2014
Ordered.v		Ordered.v	Update LICENSE file and headers for dual-licensed files.	Jun 17, 2013
Parmov.v		Parmov.v	Silence the warning "Cannot build inversion information".	Feb 24, 2014
Postorder.v		Postorder.v	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	Jan 29, 2013
Tokenize.mli		Tokenize.mli	Cleaner, more resilient parsing of pragmas.	Jun 5, 2014
Tokenize.mll		Tokenize.mll	Cleaner, more resilient parsing of pragmas.	Jun 5, 2014
UnionFind.v		UnionFind.v	Assorted cleanups, esp. to avoid generating _rec and _rect recursors in	Mar 9, 2013
Wfsimpl.v		Wfsimpl.v	Merge of the newmem branch:	May 21, 2012
View all files