aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Merge PR#826: Put plugin exports in the right compatibility fileGravatar Maxime Dénès2017-06-26
|\
* \ Merge PR#794: Cleanup of ltac cmxsGravatar Maxime Dénès2017-06-23
|\ \
| | * Put plugin exports in the right compatibility fileGravatar Jason Gross2017-06-22
| |/ |/|
| * plugins/ltac : avoid spurious .cmxs filesGravatar Pierre Letouzey2017-06-15
* | Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\ \ | |/ |/|
* | Merge PR#753: Fix bug 5026 (the stdlib shouldn't define inconsistent notations).Gravatar Maxime Dénès2017-06-14
|\ \
* | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| | * Remove deprecated options from the standard library.Gravatar Guillaume Melquiond2017-06-14
| | * Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| |/ |/|
* | Merge PR#498: Bignums as a separate opam packageGravatar Maxime Dénès2017-06-14
|\ \
* \ \ Merge PR#385: Equality of sigma typesGravatar Maxime Dénès2017-06-13
|\ \ \
| | * | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
| |/ / |/| |
* | | Remove remaining vo.itarget files (obsolete since PR #499)Gravatar Pierre Letouzey2017-06-10
| | * Fix bug 5026 (the stdlib shouldn't define inconsistent notations).Gravatar Théo Zimmermann2017-06-08
| |/ |/|
* | 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
|/
* 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
|/ /
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 21:54:33 +0000