aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib/index-list.html.template
AgeCommit message (Expand)Author
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
2018-07-16bin,oct,hex conversions positive,Z,N,nat<->stringJason Gross
2018-03-07Add empty compat file for Coq 8.8Jason Gross
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-02-20Doc: add Decimal-related files to index-list.html.templateJason Gross
2017-07-21Adding a V8.7 compatibility version number.Hugo Herbelin
2017-06-14Remove support for Coq 8.4.Guillaume Melquiond
2017-06-13BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Pierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 16:36:23 +0000