index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2020-05-11
Merge PR #10609: Register (for Coqlib.ref_lib) several base datatypes of stdlib
Hugo Herbelin
2020-05-11
Checking validity of coqdoc file name.
Hugo Herbelin
2020-05-11
Merge PR #12273: Deprecate Refiner API
Emilio Jesus Gallego Arias
2020-05-11
Correcting ltac2's documentation on values turning test into proper check.
Kenji Maillard
2020-05-11
Generalize the Ltac2 value criterion to pure let-bindings.
Pierre-Marie Pédrot
2020-05-11
Allow to rebind the old value of a mutable Ltac2 entry.
Pierre-Marie Pédrot
2020-05-11
Merge PR #12129: Add a `with_strategy` tactic
Pierre-Marie Pédrot
2020-05-10
Remove (outdated) timestamps from man pages
Kartik Singhal
2020-05-10
Add overlays.
Pierre-Marie Pédrot
2020-05-10
Further cleanup: remove the local_reduction_function type.
Pierre-Marie Pédrot
2020-05-10
No more local reduction functions in Reductionops.
Pierre-Marie Pédrot
2020-05-10
Merge PR #12235: Ensure eintros allows creating evars
Kenji Maillard
2020-05-10
Merge PR #12287: Define CRzero and CRone via CR_of_Q
Michael Soegtrop
2020-05-10
Change log for #12223.
Hugo Herbelin
2020-05-10
Adding tests for error location
Hugo Herbelin
2020-05-10
Locating error again in TacAtom and TacAlias (fixes #12152, fixes #12255).
Hugo Herbelin
2020-05-10
Merge PR #12286: [sphinx] Add links to other versions of the refman
Théo Zimmermann
2020-05-09
[sphinx] Add links to other versions of the refman
Clément Pit-Claudel
2020-05-09
Merge PR #12241: [declare] Merge DeclareDef into Declare
Gaëtan Gilbert
2020-05-09
Add another note about removing a tactic after abstract
Jason Gross
2020-05-09
Revert "[with_strategy] Fix for coqchk"
Jason Gross
2020-05-09
[with_strategy] Fix for coqchk
Jason Gross
2020-05-09
Fix a bug with with_strategy, behavior on multisuccess tactics
Jason Gross
2020-05-09
[with_strategy] Work around #12191
Jason Gross
2020-05-09
Work around a bug in Coq in the doc
Jason Gross
2020-05-09
Elaborate with_strategy warning
Jason Gross
2020-05-09
Fix the `with_strategy` tactic to work with `abstract`
Jason Gross
2020-05-09
Add a `with_strategy` tactic
Jason Gross
2020-05-09
Add overlays
Pierre Roux
2020-05-09
Hexadecimal: conversion to/from Coq strings
Pierre Roux
2020-05-09
Hexadecimal: proofs that conversions from/to nat,N,Z and Q are bijections
Pierre Roux
2020-05-09
[doc] Add hexadecimal numerals
Pierre Roux
2020-05-09
Add hexadecimal numerals
Pierre Roux
2020-05-09
Rename functions
Pierre Roux
2020-05-09
Add helper function
Pierre Roux
2020-05-09
Decimal: prove numeral notation for Q
Pierre Roux
2020-05-09
Decimal: specify numeral notation for Q
Pierre Roux
2020-05-09
Uniformize indentation in theories/Numbers
Pierre Roux
2020-05-09
NumTok.int doesn't exist anymore
Pierre Roux
2020-05-09
Define CRzero and CRone via CR_of_Q
Vincent Semeria
2020-05-09
Merge PR #12204: Ltac helper functions API
Hugo Herbelin
2020-05-09
Merge PR #12237: [stdlib] [List] add results around incl, filter and nth
Hugo Herbelin
2020-05-09
Merge PR #12163: Fix #12159 (Numeral Notations do not play well with multiple...
Hugo Herbelin
2020-05-09
Merge PR #12040: Document the signing procedure of released binary packages.
Maxime Dénès
2020-05-09
Merge PR #12122: Avoid registering as keywords the #... in Primitive
Maxime Dénès
2020-05-09
Merge PR #11990: [micromega] use Coqlib.lib_ref to get Coq constants.
Maxime Dénès
2020-05-08
Merge PR #12272: Cleanup formatting in .. coqtop:: directives
Clément Pit-Claudel
2020-05-09
Merge PR #12263: HaskellExtr: Add type annotations to Prelude.==
Kazuhiko Sakaguchi
2020-05-08
Recursively look for the first string node
Quentin Carbonneaux
2020-05-08
Declare more Permutation instances as Global
Olivier Laurent
[prev]
[next]