aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib/index-list.html.template
AgeCommit message (Expand)Author
2020-12-02Merge PR #13275: Put all Int63 primitives in a separate fileVincent Laporte
2020-12-02Put all Int63 primitives in a separate filePierre Roux
2020-11-23Update compat infrastructure for 8.14Enrico Tassi
2020-11-09[compat] remove 8.10Enrico Tassi
2020-11-05[numeral notation] Specify RPierre Roux
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-07-06Primitive persistent arraysMaxime Dénès
2020-05-18Update to 8.13.Théo Zimmermann
2020-05-16Prove that classical reals implement constructive reals. Also move sums, min ...Vincent Semeria
2020-05-09Hexadecimal: conversion to/from Coq stringsPierre Roux
2020-05-09Hexadecimal: proofs that conversions from/to nat,N,Z and Q are bijectionsPierre Roux
2020-05-09[doc] Add hexadecimal numeralsPierre Roux
2020-05-09Decimal: specify numeral notation for QPierre Roux
2020-05-04add order properties about boolOlivier Laurent
2020-04-22Merge PR #12031: [stdlib] A library on cyclic permutations: CPermutationHugo Herbelin
2020-04-21Adding a Declare ML Module in empty file Ltac.v.Hugo Herbelin
2020-04-19A library on cyclic permutations: CPermutationOlivier Laurent
2020-04-01- Adjusted definitions and lemmas for asin and acos to what has been discussedMichael Soegtrop
2020-03-27Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move Cons...Vincent Semeria
2020-03-04Add file to register names of reals library used by gappaMichael Soegtrop
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
2020-02-08Remove -compat 8.9.Théo Zimmermann
2020-01-17[doc] [dune] [ltac2] Build Ltac2 documentation [dune build system]Emilio Jesus Gallego Arias
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-11Run update-compat script with --release option.Théo Zimmermann
2019-11-01Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) r...Enrico Tassi
2019-11-01docs: Add refman+stdlib documentationErik Martin-Dorel
2019-10-27Merge PR #10827: Replace classical reals quotient axioms by functional extens...Hugo Herbelin
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ...Vincent Semeria
2019-10-07Call to update-compat.py.Pierre-Marie Pédrot
2019-09-16Define morphisms of real numbers and accelerate Cauchy realsVincent Semeria
2019-08-19Split ConstructiveRealsLUB and improve commentsVincent Semeria
2019-08-08Add interface of constructive real numbers, with an opaque implementation by ...Vincent Semeria
2019-08-08[ssr] Refactor under's Setoid generalization to ease stdlib2 portingErik Martin-Dorel
2019-08-05Merge PR #10445: Split constructive and classical axioms for real numbersVincent Laporte
2019-07-26[stdlib] Remove deprecated module Zsqrt_compatVincent Laporte
2019-07-26[stdlib] Remove deprecated module ZlogarithmVincent Laporte
2019-07-17Rename ConstructiveRIneq and ConstructiveRcompleteVincent Semeria
2019-07-16Define constructive real numbers as Cauchy sequences of rational numbers. Red...Vincent Semeria
2019-04-02Remove -compat 8.7Jason Gross
2019-03-14Add StrictProp.v with basic SProp related definitionsGaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2019-01-24Update -compat to support -compat 8.10Jason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
2018-11-16Merge PR #8888: Proof runcountable rebaseHugo Herbelin
2018-11-07[doc] also scan plugins/ to build the lirbary indexEnrico Tassi
2018-11-01Fix header and doc indexVincent Semeria
2018-10-17doc: mention ByteVectorYishuai Li
2018-10-02Update the -compat flagsJason Gross
2018-08-31Numeral Notation for natPierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:00:33 +0000