aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init
Commit message (Expand)AuthorAge
* Merge PR #6820: Tacticals assert_fails and assert_succeedsGravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6522: Fix core hint database issue #6521Gravatar Maxime Dénès2018-03-08
|\ \
* \ \ Merge PR #6743: Add notation {x & P} for sigTGravatar Maxime Dénès2018-03-08
|\ \ \
* \ \ \ Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ \ \
* | | | | Remove the deprecation for some 8.2-8.5 compatibility aliases.Gravatar Théo Zimmermann2018-03-02
| | | | * Uniform spacing layout in Tactics.v.Gravatar Hugo Herbelin2018-02-28
| | | | * Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).Gravatar Hugo Herbelin2018-02-28
| * | | | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/ / / /
* | | | Merge PR #6599: Decimals in preludeGravatar Maxime Dénès2018-02-24
|\ \ \ \ | |_|_|/ |/| | |
| * | | Decimal: proofs that conversions from/to nat,N,Z are bijectionsGravatar Pierre Letouzey2018-02-20
| * | | Decimal: simple representation of base-10 numbersGravatar Pierre Letouzey2018-02-20
* | | | Trying a hack to support {'pat|P} without breaking compatibility.Gravatar Hugo Herbelin2018-02-20
* | | | Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.Gravatar Hugo Herbelin2018-02-20
* | | | User-level support for Gonthier-Ssreflect's "if t then pat then u else v".Gravatar Hugo Herbelin2018-02-20
|/ / /
| * / Add notation {x & P} for sigTGravatar Tej Chajed2018-02-12
|/ /
| * Fix core hint database issue #6521Gravatar Anton Trunov2018-01-03
|/
* Add named timers to LtacProfGravatar Jason Gross2017-12-14
* Moving bug numbers to BZ# format in the source code.Gravatar Théo Zimmermann2017-10-19
* A little reorganization of notations + a fix to #5608.Gravatar Hugo Herbelin2017-08-29
* Fix typo in documentation for identityGravatar Tej Chajed2017-07-05
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* plugins/ltac : avoid spurious .cmxs filesGravatar Pierre Letouzey2017-06-15
* Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
* Merge PR#385: Equality of sigma typesGravatar Maxime Dénès2017-06-13
|\
* | drop vo.itarget files and compute the corresponding the corresponding values ...Gravatar Matej Kosik2017-06-01
| * More uniform indentation of sigma lemmasGravatar Jason Gross2017-05-28
| * Give explicit proof terms to proj2_sig_eq etc.Gravatar Jason Gross2017-05-28
| * Use the rew dependent notation in ex, ex2 proofsGravatar Jason Gross2017-05-28
| * Make theorems about ex equality QedGravatar Jason Gross2017-05-28
| * Make new proofs of equality QedGravatar Jason Gross2017-05-28
| * Add some more comments about sigma equalitiesGravatar Jason Gross2017-05-28
| * Remove motive argument from [rew dependent]Gravatar Jason Gross2017-05-28
| * Use a local [rew dependent] notationGravatar Jason Gross2017-05-28
| * Add forward-chaining versions: [eq_sig*_uncurried]Gravatar Jason Gross2017-05-28
| * Use notation for sigTGravatar Jason Gross2017-05-28
| * Remove reference to [IsIso]Gravatar Jason Gross2017-05-28
| * Use notations for [sig], [sigT], [sig2], [sigT2]Gravatar Jason Gross2017-05-28
| * Use extended notation for ex, ex2 typesGravatar Jason Gross2017-05-28
| * Replace [ex'] with [ex]Gravatar Jason Gross2017-05-28
| * Use [rew_] instead of [eq_rect_] prefixGravatar Jason Gross2017-05-28
| * Add equality lemmas for sig2 and sigT2Gravatar Jason Gross2017-05-28
| * Add lemmas for ex2Gravatar Jason Gross2017-05-28
| * Use [rew] notations rather than [eq_rect]Gravatar Jason Gross2017-05-28
| * Add an [inversion_sigma] tacticGravatar Jason Gross2017-05-28
| * Add lemmas about equality of sigma typesGravatar Jason Gross2017-05-28
| * Use [rew_] instead of [eq_rect_] prefixGravatar Jason Gross2017-05-28
| * Use [rew] notations rather than [eq_rect]Gravatar Jason Gross2017-05-28
| * Add more groupoid-like theorems about [eq]Gravatar Jason Gross2017-05-28
|/
* Merge PR#201: Transparent abstractGravatar Maxime Dénès2017-05-11
|\
* \ Merge PR#605: Report a useful error for dependent inductionGravatar Maxime Dénès2017-05-05
|\ \