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 #7690: Fixing typos in file Berardi.v
Pierre-Marie Pédrot
2018-06-05
|
\
*
|
Deprecate implicit tactic solving.
Pierre-Marie Pédrot
2018-06-04
|
*
Fixing typos in file Berardi.v
Hugo Herbelin
2018-06-03
|
/
*
Protecting against a "deprecated cofix" warning.
Hugo Herbelin
2018-04-16
*
[ltac] Deprecate nameless fix/cofix.
Emilio Jesus Gallego Arias
2018-04-13
*
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
|
|
/
/
/
|
/
|
|
|
[next]
Pierre-Marie Pédrot
Hugo Herbelin
Emilio Jesus Gallego Arias
Maxime Dénès
Vincent Laporte
Jason Gross
Théo Zimmermann
Pierre Letouzey
Tej Chajed
Ismail
Gaëtan Gilbert
Anton Trunov
Jasper Hugunin
Jasper Hugunin
Joachim Breitner
fredokun