aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-09Add hexadecimal numeralsPierre Roux
2020-05-09Rename functionsPierre Roux
2020-05-09Add helper functionPierre Roux
2020-05-09Decimal: prove numeral notation for QPierre Roux
2020-05-09Decimal: specify numeral notation for QPierre Roux
2020-05-09Uniformize indentation in theories/NumbersPierre Roux
2020-05-09NumTok.int doesn't exist anymorePierre Roux
2020-05-09Define CRzero and CRone via CR_of_QVincent Semeria
2020-05-09Merge PR #12204: Ltac helper functions APIHugo Herbelin
2020-05-09Merge PR #12237: [stdlib] [List] add results around incl, filter and nthHugo Herbelin
2020-05-09Merge PR #12163: Fix #12159 (Numeral Notations do not play well with multiple...Hugo Herbelin
2020-05-09Merge PR #12040: Document the signing procedure of released binary packages.Maxime Dénès
2020-05-09Merge PR #12122: Avoid registering as keywords the #... in PrimitiveMaxime Dénès
2020-05-09Merge PR #11990: [micromega] use Coqlib.lib_ref to get Coq constants.Maxime Dénès
2020-05-08Merge PR #12272: Cleanup formatting in .. coqtop:: directivesClément Pit-Claudel
2020-05-09Merge PR #12263: HaskellExtr: Add type annotations to Prelude.==Kazuhiko Sakaguchi
2020-05-08Recursively look for the first string nodeQuentin Carbonneaux
2020-05-08Declare more Permutation instances as GlobalOlivier Laurent
2020-05-08In non-strict mode, accept any variable as a tactic reference.Pierre-Marie Pédrot
2020-05-08Simplify splittingQuentin Carbonneaux
2020-05-08Merge PR #12281: [doc] named lemmas can be Saved tooThéo Zimmermann
2020-05-08Merge PR #12268: Add an example to motivate strictly positive occurrences checkThéo Zimmermann
2020-05-08Merge PR #12068: Coqide completion: tentative fix for #11943Pierre-Marie Pédrot
2020-05-08Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpointsPierre-Marie Pédrot
2020-05-08doc: one can save named lemmas Save tooAntonio Nikishaev
2020-05-07rename Bool.leb into Bool.le (same for ltb and compareb)Olivier Laurent
2020-05-07[win] CI build addons Coq-Elpi Hierarchy-BuilderEnrico Tassi
2020-05-07[win] addon for Hierarchy BuilderEnrico Tassi
2020-05-07[win] addon for elpiEnrico Tassi
2020-05-07[declare] Merge DeclareDef into DeclareEmilio Jesus Gallego Arias
2020-05-07[declare] Remove fix_exn internal access.Emilio Jesus Gallego Arias
2020-05-07Deprecate the legacy tacticals from module Refiner.Pierre-Marie Pédrot
2020-05-07Remove call to Refiner API from Funind.Pierre-Marie Pédrot
2020-05-07Port Evar_tactics to the new API.Pierre-Marie Pédrot
2020-05-07Merge PR #12236: [funind] Remove use of low-level entries in scheme generation.Gaëtan Gilbert
2020-05-07Merge PR #12262: Fix #12211 (TIMED for ocaml files doesn't print file name)Gaëtan Gilbert
2020-05-07Merge PR #12024: Fixes for LaTeX/html export of standard library in coqdocThéo Zimmermann
2020-05-07[win] rules to build ElpiEnrico Tassi
2020-05-07[win] bump camlp5 to 7.11 since OCaml 4.08 requires itEnrico Tassi
2020-05-07[win] since 4.07 the seq package is part of ocamlEnrico Tassi
2020-05-07[win] Coq trunk is now called masterEnrico Tassi
2020-05-07Cleanup formatting in .. coqtop:: directivesQuentin Carbonneaux
2020-05-07Merge PR #12267: [ci] bump elpi to 1.11Emilio Jesus Gallego Arias
2020-05-07Documenting the new behavior of "subst".Hugo Herbelin
2020-05-07Adding change log for #12146.Hugo Herbelin
2020-05-07Tactic subst now inactive on section variables occurring indirectly in goal.Hugo Herbelin
2020-05-07Termops: Adding functions local_occur_var_in_decl and occur_var_indirectly.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 11:28:20 +0000