aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
...
| * 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
|/
* Stop using auto with * in two proofs.Gravatar Théo Zimmermann2017-05-16
* 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
|\ \
* \ \ Merge PR#593: Functional choice <-> [inhabited] and [forall] commuteGravatar Maxime Dénès2017-05-05
|\ \ \
* \ \ \ Merge PR#588: Allow interactive editing of {C,}Morphisms in PGGravatar Maxime Dénès2017-05-03
|\ \ \ \
* \ \ \ \ Merge PR#386: Better editing of the standard library in coqtop/PGGravatar Maxime Dénès2017-05-03
|\ \ \ \ \
| | | | * | Report a useful error for dependent inductionGravatar Tej Chajed2017-05-03
| |_|_|/ / |/| | | |
| | | * | Reorganize comment documentation of ChoiceFacts.vGravatar Gaetan Gilbert2017-05-03
| | | * | Functional choice <-> [inhabited] and [forall] commuteGravatar Gaetan Gilbert2017-04-30
| |_|/ / |/| | |
* | | | Suppress warning message in stdlib.Gravatar Guillaume Melquiond2017-04-29
| | * | Allow interactive editing of {C,}Morphisms in PGGravatar Jason Gross2017-04-28
| |/ / |/| |
| * | Add .dir-locals.el and _CoqProject files for emacs stdlib editingGravatar Jason Gross2017-04-28
|/ /
* | Merge PR#414: Some more theory on powerRZ.Gravatar Maxime Dénès2017-04-27
|\ \
* \ \ Merge PR#584: Give andb_prop a simpler proofGravatar Maxime Dénès2017-04-27
|\ \ \
* | | | Small typo in commentGravatar Vadim Zaliva2017-04-26
| | | * Add transparent_abstract tacticGravatar Jason Gross2017-04-25
| |_|/ |/| |
| * | Give andb_prop a simpler proofGravatar Jason Gross2017-04-25
|/ /
* | Merge PR#545: Add some hints to the "real" database to automatically discharg...Gravatar Maxime Dénès2017-04-19
|\ \
* \ \ Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\ \ \
| | * | Add some hints to the "real" database to automatically discharge literal comp...Gravatar Guillaume Melquiond2017-04-07
| |/ / |/| |
* | | Merge PR#455: Farewell decl_modeGravatar Maxime Dénès2017-04-06
|\ \ \
| | * \ Merge branch 'origin/v8.5' into v8.6.Gravatar Hugo Herbelin2017-04-06
| | |\ \
* | | | | Fix documentation typo (bug #5433).Gravatar Guillaume Melquiond2017-04-02
* | | | | Simplify some proofs.Gravatar Guillaume Melquiond2017-04-02
* | | | | Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.Gravatar Guillaume Melquiond2017-03-30
* | | | | Merge PR#469: Added take to VectorDefGravatar Maxime Dénès2017-03-30
|\ \ \ \ \
| * | | | | Added take to VectorDef.Gravatar George Stelle2017-03-30
* | | | | | Fixing missing PropFacts.v in Logic/vo.itarget.Gravatar Hugo Herbelin2017-03-28
* | | | | | Merge PR#392: strengthened the statement of JMeq_eq_depGravatar Maxime Dénès2017-03-24
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
|\ \ \ \ \ \ \ | | |_|_|/ / / | |/| | | | |
* | | | | | | Make IZR a morphism for field.Gravatar Guillaume Melquiond2017-03-22
* | | | | | | Change the parser and printer so that they use IZR for real constants.Gravatar Guillaume Melquiond2017-03-22
* | | | | | | Make IZR use a compact representation of integers.Gravatar Guillaume Melquiond2017-03-22
* | | | | | | Simplify some proofs using ring and field.Gravatar Guillaume Melquiond2017-03-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 22:48:31 +0000