aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
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-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
2018-09-10Merge PR #8230: fix formulation of the Euclid Theorem in commentHugo Herbelin
2018-09-10Declaring Scope prior to loading primitive printers.Hugo Herbelin
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-09-10Deprecate romega in favor of lia.Vincent Laporte
2018-09-07Bvector: add BVeq and some notationsYishuai Li
2018-09-07NArith: deprecate N2Bv_genYishuai Li
2018-09-06Bound proof-search in default program obligation tactic.Matthieu Sozeau
2018-08-31Make Numeral Notation follow Import, not RequireJason Gross
2018-08-31Fix numeral notation for a rebase on top of masterJason Gross
2018-08-31Decimal: scope name changed dec_(u)int_scopePierre Letouzey
2018-08-31Numeral Notation for natPierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 03:17:28 +0000