aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2019-01-24Make `Instance` without a body always open a proof.Maxime Dénès
2019-01-23Pass some files to strict focusing mode.Gaëtan Gilbert
2019-01-22Turn `Refine Instance Mode` off by defaultMaxime Dénès
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
2018-12-12Merge PR #9087: Add CI job building stdlib with `async-proofs on`Emilio Jesus Gallego Arias
2018-12-12Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`Hugo Herbelin
2018-12-12Avoid Fixpoint without struct nor body in stdlibMaxime Dénès
2018-12-10Merge PR #7221: The usual order of strings.Hugo Herbelin
2018-11-30Merge PR #8807: Added two proofs to the Lists library: Forall_inv_tail and Ex...Pierre-Marie Pédrot
2018-11-28Byte.v: use right-associative tuples in bitsJason Gross
2018-11-28Proofs to ensure that conversions round-tripJason Gross
2018-11-28Speed up ByteJason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
2018-11-28Merge PR #7153: Make OrderedTypeFullFacts a module functorGaëtan Gilbert
2018-11-27Added two proofs to the Lists library. The first, Forall_inv_tail, extends Fo...llee454@gmail.com
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-22The usual order of strings.Yao Li
2018-11-22Disable deprecation warnings in compat files.Gaëtan Gilbert
2018-11-19Merge PR #8987: Deprecate hint declaration/removal with no specified databasePierre-Marie Pédrot
2018-11-16Merge PR #8888: Proof runcountable rebaseHugo Herbelin
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-11-13Merge PR #8886: [VM] Fix compilation of int31 eliminatorsMaxime Dénès
2018-11-11Merge PR #8795: Encapsulating declarations of primitive string syntax in a mo...Jason Gross
2018-11-08[VM] Fix compilation of int31 eliminatorsVincent Laporte
2018-11-01develop constructive epsilonVincent Semeria
2018-11-01Fix header and doc indexVincent Semeria
2018-11-01proof that R is uncountableVincent Semeria
2018-10-29NArith: implicit length argument for Bv2NYishuai Li
2018-10-29NArith: add lemmas about numbers and vectorsYishuai Li
2018-10-23Compat 8.8: For String/Ascii, hides "Declare ML Module" behind an "Export".Hugo Herbelin
2018-10-23Encapsulating declarations of primitive string syntax in a module.Hugo Herbelin
2018-10-17Strings: add ByteVectorYishuai Li
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-02Update the -compat flagsJason Gross
2018-10-02Update compat notations to be compat 8.7Jason Gross
2018-10-01Merge PR #7372: Four new lemmas for listsHugo Herbelin
2018-10-01Merge PR #517: Some lemmas about dependent equalityPierre-Marie Pédrot
2018-09-29New lemmas for List.vSimon Marechal
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-25Merge PR #8235: NArith: deprecate N2Bv_genHugo Herbelin
2018-09-25Adding lemmas about dependent equality.Hugo Herbelin
2018-09-25Mini refreshing layout Datatypes.v.Hugo Herbelin
2018-09-25Adding f_equal_dep in Logic.v.Hugo Herbelin
2018-09-22Fix typo in comment.Nick Lewycky
2018-09-14Register: simpler syntaxVincent Laporte
2018-09-14Retroknowledge: remove the (unused) by clauseVincent Laporte
2018-09-14Retroknowledge.KInt31: remove the (unused) group parameterVincent Laporte
2018-09-11Merge PR #8425: Deprecate romega in favor of liaPierre-Marie Pédrot
2018-09-11Merge PR #7135: Introducing an explicit `Declare Scope` commandEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 00:42:26 +0000