index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
Commit message (
Expand
)
Author
Age
*
Merge PR #6820: Tacticals assert_fails and assert_succeeds
Maxime Dénès
2018-03-09
|
\
*
\
Merge PR #6155: Get rid of ' notation for Zpos in QArith
Maxime Dénès
2018-03-09
|
\
\
*
\
\
Merge PR #6937: Add empty compat file for Coq 8.8
Maxime Dénès
2018-03-09
|
\
\
\
*
\
\
\
Merge PR #6522: Fix core hint database issue #6521
Maxime Dénès
2018-03-08
|
\
\
\
\
*
\
\
\
\
Merge PR #6743: Add notation {x & P} for sigT
Maxime Dénès
2018-03-08
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6909: Deprecate Focus and Unfocus
Maxime Dénès
2018-03-08
|
\
\
\
\
\
\
*
|
|
|
|
|
|
[stdlib] Do not use “Require” inside sections
Vincent Laporte
2018-03-07
|
|
|
|
*
|
|
Add empty compat file for Coq 8.8
Jason Gross
2018-03-07
|
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR #6744: Add String.concat
Maxime Dénès
2018-03-07
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-05
|
\
\
\
\
\
\
\
|
|
|
*
|
|
|
|
Remove all uses of Focus in standard library.
Théo Zimmermann
2018-03-04
*
|
|
|
|
|
|
|
Remove 8.5 compatibility support.
Théo Zimmermann
2018-03-02
*
|
|
|
|
|
|
|
Remove VOld compatibility flag.
Théo Zimmermann
2018-03-02
*
|
|
|
|
|
|
|
Turn warning for deprecated notations on.
Théo Zimmermann
2018-03-02
*
|
|
|
|
|
|
|
Remove the deprecation for some 8.2-8.5 compatibility aliases.
Théo Zimmermann
2018-03-02
|
|
_
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
*
Uniform spacing layout in Tactics.v.
Hugo Herbelin
2018-02-28
|
|
|
|
|
|
*
Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).
Hugo Herbelin
2018-02-28
*
|
|
|
|
|
|
Merge PR #6852: [stdlib] move “Require” out of sections
Maxime Dénès
2018-02-28
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmas
Maxime Dénès
2018-02-28
|
\
\
\
\
\
\
\
\
|
|
|
*
|
|
|
|
|
Update headers following #6543.
Théo Zimmermann
2018-02-27
|
|
_
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
[stdlib] move “Require” out of sections
Vincent Laporte
2018-02-27
|
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
Add String.concat
Jason Gross
2018-02-24
|
|
/
/
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR #6599: Decimals in prelude
Maxime Dénès
2018-02-24
|
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_pred
Maxime Dénès
2018-02-21
|
\
\
\
\
\
\
|
|
*
|
|
|
|
Decimal goodies : conversion to/from Coq strings
Pierre Letouzey
2018-02-20
|
|
*
|
|
|
|
Decimal: proofs that conversions from/to nat,N,Z are bijections
Pierre Letouzey
2018-02-20
|
|
*
|
|
|
|
Decimal: simple representation of base-10 numbers
Pierre Letouzey
2018-02-20
*
|
|
|
|
|
|
Trying a hack to support {'pat|P} without breaking compatibility.
Hugo Herbelin
2018-02-20
*
|
|
|
|
|
|
Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.
Hugo Herbelin
2018-02-20
*
|
|
|
|
|
|
More structured printing in unicode notations for binders.
Hugo Herbelin
2018-02-20
*
|
|
|
|
|
|
User-level support for Gonthier-Ssreflect's "if t then pat then u else v".
Hugo Herbelin
2018-02-20
|
|
/
/
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
|
|
|
|
*
|
|
Add notation {x & P} for sigT
Tej Chajed
2018-02-12
|
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR #6139: Make list functions returning sumbools transparent
Maxime Dénès
2018-02-12
|
\
\
\
\
\
\
*
|
|
|
|
|
|
Document between and exists_between types.
Ismail
2018-01-08
|
|
*
|
|
|
|
Remove dir-locals and ship suggested helper hooks instead.
Gaëtan Gilbert
2018-01-06
|
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
Fix core hint database issue #6521
Anton Trunov
2018-01-03
|
|
_
|
_
|
/
/
|
/
|
|
|
|
*
|
|
|
|
Fix warning about shadowing a global name.
Gaëtan Gilbert
2017-12-19
*
|
|
|
|
Add named timers to LtacProf
Jason Gross
2017-12-14
*
|
|
|
|
Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_facts
Maxime Dénès
2017-12-12
|
\
\
\
\
\
*
|
|
|
|
|
Axiom-free proof of eta expansion.
Jasper Hugunin
2017-12-11
*
|
|
|
|
|
Remove most uses of function extensionality in Program.Combinators
Jasper Hugunin
2017-12-09
|
*
|
|
|
|
Additional rewrite lemmas on Ensembles, in Powerset_facts
Joachim Breitner
2017-12-06
|
/
/
/
/
/
|
|
*
|
|
proposed fix for issue #3213: extra variable m in Lt.S_pred
fredokun
2017-12-01
*
|
|
|
|
Fix (partial) #4878: option to stop autodeclaring axiom as instance.
Gaëtan Gilbert
2017-11-28
|
|
/
/
/
|
/
|
|
|
|
*
|
|
Make list functions returning sumbools transparent
Tej Chajed
2017-11-15
|
/
/
/
|
|
*
Get rid of ' notation for Zpos in QArith.
Robbert Krebbers
2017-11-14
|
|
/
|
/
|
*
|
Merge PR #1113: Adding 3 Arith/QArith lemmas that I found useful
Maxime Dénès
2017-10-27
|
\
\
|
*
|
Chaining two tactics in a proof
Raphaël Monat
2017-10-27
|
*
|
Moving from `is_true` to `= true`
Raphaël Monat
2017-10-25
[next]
Maxime Dénès
Vincent Laporte
Jason Gross
Théo Zimmermann
Hugo Herbelin
Pierre Letouzey
Tej Chajed
Ismail
Gaëtan Gilbert
Anton Trunov
Jasper Hugunin
Jasper Hugunin
Joachim Breitner
fredokun
Robbert Krebbers
Raphaël Monat