aboutsummaryrefslogtreecommitdiff
path: root/theories/Bool
AgeCommit message (Expand)Author
2020-12-15Modify Bool/Zerob.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Bool/IfProp.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Bool/DecBool.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Bool/BoolEq.v to compile with -mangle-namesJasper Hugunin
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-10-09Modify Bool/Sumbool.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Bool/Bool.v to compile with -mangle-namesJasper Hugunin
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
2020-05-07rename Bool.leb into Bool.le (same for ltb and compareb)Olivier Laurent
2020-05-06Merge PR #12008: [stdlib] Add order properties about boolAnton Trunov
2020-05-06Layout of Bool.v, especially for coqdoc.Hugo Herbelin
2020-05-06Adding properties about implb.Hugo Herbelin
2020-05-04add order properties about boolOlivier Laurent
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-08-25Make Bool.eqb_spec transparentTej Chajed
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-01-23Pass some files to strict focusing mode.Gaëtan Gilbert
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-09-27[stdlib] Fix warning due to missing Declare Scope in BvectorEmilio Jesus Gallego Arias
2018-09-26Merge PR #8171: Bvector: add BVeq and some notationsHugo Herbelin
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-09-07Bvector: add BVeq and some notationsYishuai Li
2018-07-16Ascii.eqb and String.eqbPierre Letouzey
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ...Matej Kosik
2016-10-24Remove v62 from stdlib.Théo Zimmermann
2016-01-20Update copyright headers.Maxime Dénès
2015-07-31Remove some outdated files and fix permissions.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-10-22Fixing typo absorption (bug #3751).Hugo Herbelin
2014-05-02Eta contractions to please cbnPierre Boutillier
2012-08-08Updating headers.herbelin
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-06-21Follow-up concerning eqb / ltb / leb comparisonsletouzey
2010-12-10First release of Vector library.pboutill
2010-12-06Numbers and bitwise functions.letouzey
2010-11-18Some more revision of {P,N,Z}Arith + bitwise ops in Ndigitsletouzey
2010-10-23Used multiple lists of implicit arguments to transfer the choices ofherbelin
2010-09-28Bvector.Vshiftin was wrong for agespboutill
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-18Reverted 13293 commited mistakenly. Sorry for the noise.herbelin
2010-07-18Tentative de suppression de l'import automatique des hints et coercions.herbelin
2010-07-16Bool: shorter and more systematic proofs + an iff lemma about eqbletouzey
2010-07-10Bool: iff lemmas about or, a reflect inductive, an is_true functionletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-02-17Kill some useless dependencies (Bvector, Program.Syntax)letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:41:49 +0000