aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* | Continuing 003fe3d5e on parsing positions.Gravatar Hugo Herbelin2016-01-14
* | Changing "P is assumed" to "P is declared".Gravatar Hugo Herbelin2016-01-14
* | Update in the documentation of parts of the code of destruct/induction.Gravatar Hugo Herbelin2016-01-14
| * MMaps: remove it from final 8.5 release, since this new library isn't mature ...Gravatar Pierre Letouzey2016-01-13
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\|
| * Fixing success of test for #3848 after move to directory "closed".Gravatar Hugo Herbelin2016-01-13
| * Fixing #4467 (continued).Gravatar Hugo Herbelin2016-01-13
| * Fixing #4467 (missing shadowing of variables in cases pattern).Gravatar Hugo Herbelin2016-01-12
| * Fixing #4256 and #4484 (changes in evar-evar resolution made that newGravatar Hugo Herbelin2016-01-12
| * Reporting about the new tactical unshelve.Gravatar Hugo Herbelin2016-01-12
| * Extend last commit: keyed unification uses full conversions on the applied co...Gravatar Matthieu Sozeau2016-01-12
| * Extend Keyed Unification tests with the one from R. Krebbers.Gravatar Matthieu Sozeau2016-01-12
| * Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Gravatar Matthieu Sozeau2016-01-12
| * Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.Gravatar Hugo Herbelin2016-01-12
| * Documenting dtauto and dintuition.Gravatar Hugo Herbelin2016-01-12
| * Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding".Gravatar Hugo Herbelin2016-01-12
| * Documenting option 'Set Bracketing Last Introduction Pattern'.Gravatar Hugo Herbelin2016-01-12
| * restore documentation of admitGravatar Enrico Tassi2016-01-12
* | CLEANUP: removing unnecessary wrapperGravatar Matej Kosik2016-01-11
* | COMMENTS: added to the "Constrexpr.CCases" variant.Gravatar Matej Kosik2016-01-11
* | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
| | * Fix bug #3338 again, no progress is necessary for the success of rewrite_strat.Gravatar Matthieu Sozeau2016-01-11
* | | COMMENTS: of "Constr.case_info" type were updated.Gravatar Matej Kosik2016-01-11
* | | COMMENTS: added to the "Names.inductive" and "Names.constructor" types.Gravatar Matej Kosik2016-01-11
* | | Fix bug 4479: "Error: Rewriting base foo does not exist." should be catchable.Gravatar Pierre-Marie Pédrot2016-01-09
* | | Monotonizing Ftactic.Gravatar Pierre-Marie Pédrot2016-01-08
| | * Be more verbose about failure to compile libraries to native code.Gravatar Guillaume Melquiond2016-01-08
| | * Fix a misleading comment for substn_varsGravatar Matthieu Sozeau2016-01-07
| | * Fix bug #4480: progress was not checked for setoid_rewrite.Gravatar Matthieu Sozeau2016-01-07
| | * Fix description of command-line options in the manual.Gravatar Guillaume Melquiond2016-01-06
* | | Remove deprecated command-line options such as "-as".Gravatar Guillaume Melquiond2016-01-06
* | | Make code more readable by not mixing list traversal and option processing.Gravatar Guillaume Melquiond2016-01-06
* | | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-06
|\ \ \ | | |/ | |/|
| * | Prevent coq_makefile from parsing project files in the reverse order. (Fix bu...Gravatar Guillaume Melquiond2016-01-06
| * | Protect code against changes in Map interface.Gravatar Maxime Dénès2016-01-06
| * | Disable warning 31 when generating coqtop from coqmktop.Gravatar Maxime Dénès2016-01-05
* | | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-05
|\ \ \
| | * | Avoid warning 31: test printer was linked twice with Dynlink and Str.Gravatar Maxime Dénès2016-01-05
| | * | Fix order of files in mllib.Gravatar Maxime Dénès2016-01-05
| |/ /
| * | COMMENTS: PredicateGravatar Matej Kosik2016-01-05
| * | fixup d2b468a, evar normalization is neededGravatar Enrico Tassi2016-01-04
| * | Extraction: msg_notice instead of msg_info.Gravatar Pierre Courtieu2016-01-04
| * | Fix handling of side-effects in case of `Opaque side-effects as well.Gravatar Matthieu Sozeau2016-01-04
| * | par: check if the goal is not ground and fail (fix #4465)Gravatar Enrico Tassi2016-01-04
| * | workers: purge short version of -load-vernac too (fix #4458)Gravatar Enrico Tassi2016-01-04
* | | Use streams rather than strings to handle bullet suggestions.Gravatar Guillaume Melquiond2016-01-02
* | | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
* | | Remove keys for evar and meta, since they cannot occur.Gravatar Guillaume Melquiond2016-01-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 08:18:56 +0000