aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Merge PR#276: Stopping injection not to work on discriminable atoms (see #4890).Gravatar Maxime Dénès2017-05-20
|\
* \ Merge PR#654: Travis: do not cache opam logs (+prettier spacing)Gravatar Maxime Dénès2017-05-20
|\ \
* \ \ Merge PR#643: [ide] Disable `print_ast` call.Gravatar Maxime Dénès2017-05-20
|\ \ \
* \ \ \ Merge PR#474: A fix for #5390 (a useful error on used introduction names was ...Gravatar Maxime Dénès2017-05-20
|\ \ \ \
* \ \ \ \ Merge PR#627: Obligations shrinking: shrink abstraction tooGravatar Maxime Dénès2017-05-20
|\ \ \ \ \
* \ \ \ \ \ Merge PR#644: [toplevel] [stm] Avoid edit_at in batch mode (bug #5520)Gravatar Maxime Dénès2017-05-20
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#648: Allow interactive editing of `plugins/` by adding .dir-locals.elGravatar Maxime Dénès2017-05-20
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR#649: Fix a typoGravatar Maxime Dénès2017-05-20
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR#651: Re-adding explicit dependency of misc universe test into all_st...Gravatar Maxime Dénès2017-05-20
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR#640: [toplevel] Restore 8.6 goal printing behavior.Gravatar Maxime Dénès2017-05-20
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | | * | Travis: do not cache opam logs (+prettier spacing)Gravatar Gaetan Gilbert2017-05-19
| |_|_|_|_|_|_|_|/ / |/| | | | | | | | |
| | * | | | | | | | Re-adding explicit dependency of misc universe test into all_stdlib.v.Gravatar Hugo Herbelin2017-05-19
| |/ / / / / / / / |/| | | | | | | |
| | * | | | | | | Fix a typoGravatar Jason Gross2017-05-18
| |/ / / / / / / |/| | | | | | |
| | * | | | | | Add .dir-locals.el to pluginsGravatar Jason Gross2017-05-18
| |/ / / / / / |/| | | | | |
| | * | | | | [toplevel] [stm] Avoid edit_at in batch mode (bug #5520)Gravatar Emilio Jesus Gallego Arias2017-05-18
| | | | | * | [ide] Disable `print_ast` call.Gravatar Emilio Jesus Gallego Arias2017-05-18
| | | |_|/ / | | |/| | |
| | | | * | A fix for #5390 (a useful error on used introduction names was masked).Gravatar Hugo Herbelin2017-05-17
| | | |/ / | | |/| |
* | | | | Merge PR#633: An extension of EXTEND and notations to make standard parsing t...Gravatar Maxime Dénès2017-05-17
|\ \ \ \ \ | |_|/ / / |/| | | |
| | | | * Documenting relaxing of constraints on injection.Gravatar Hugo Herbelin2017-05-17
| | | | * Stopping injection not to work on discriminable atoms (see #4890).Gravatar Hugo Herbelin2017-05-17
| |_|_|/ |/| | |
* | | | Merge PR#457: Adding an even more compact goal hyps mode.Gravatar Maxime Dénès2017-05-17
|\ \ \ \
* \ \ \ \ Merge PR#607: Make congruence reuse discriminate instead of rolling its own.Gravatar Maxime Dénès2017-05-17
|\ \ \ \ \
| | | | * | [toplevel] Restore 8.6 goal printing behavior.Gravatar Emilio Jesus Gallego Arias2017-05-17
* | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#620: Reorganization of the layout for miscellaneous testsGravatar Maxime Dénès2017-05-17
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR#614: Improve TravisGravatar Maxime Dénès2017-05-17
|\ \ \ \ \ \ \ \
| * | | | | | | | Travis: add -warn-error targets (standard and 4.04.1 ocaml)Gravatar Gaetan Gilbert2017-05-17
* | | | | | | | | Merge PR#630: [interp] [ast] Make raw_cases_pattern_expr private + small cleanupGravatar Maxime Dénès2017-05-17
|\ \ \ \ \ \ \ \ \
| | * | | | | | | | Travis: deduplicate package list for coqide+documentation targetsGravatar Gaetan Gilbert2017-05-17
| | * | | | | | | | Travis: do not run the tests if building Coq failsGravatar Gaetan Gilbert2017-05-17
| |/ / / / / / / / |/| | | | | | | |
| | | * | | | | | Merge PR#635: Fixing #5522 (anomaly with free vars of pat)Gravatar Maxime Dénès2017-05-17
| | | |\ \ \ \ \ \
* | | | \ \ \ \ \ \ Merge PR#636: Miscellaneous typos, dead code, etc.Gravatar Maxime Dénès2017-05-17
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR#639: Stop using auto with * in two proofs.Gravatar Maxime Dénès2017-05-17
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | |
| * | | | | | | | | | Stop using auto with * in two proofs.Gravatar Théo Zimmermann2017-05-16
|/ / / / / / / / / /
| | | | | | | | * | Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.Gravatar Hugo Herbelin2017-05-16
| | | | | | | | * | Adding support for using grammar entries returning no value in EXTEND.Gravatar Hugo Herbelin2017-05-16
| |_|_|_|_|_|_|/ / |/| | | | | | | |
| | | | | | | * | Simplified compaction criterion + tests.Gravatar Pierre Courtieu2017-05-16
| | | | | * | | | Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters).Gravatar Hugo Herbelin2017-05-16
| | | | | * | | | Fixing a bug with nested "as" clauses in "match".Gravatar Hugo Herbelin2017-05-16
| | | | * | | | | Merge PR#624: Switch bedrock to mit-plv baseGravatar Maxime Dénès2017-05-16
| | | | |\ \ \ \ \ | | | | | |/ / / / | | | | |/| | | |
* | | | | | | | | Merge PR#626: Add documentation for Set Ltac Batch DebugGravatar Maxime Dénès2017-05-16
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR#629: A couple of simple updates for TravisGravatar Maxime Dénès2017-05-16
|\ \ \ \ \ \ \ \ \ \
| | | * | | | | | | | Dead code in coqdep.Gravatar Hugo Herbelin2017-05-15
| | | | * | | | | | | [interp] Rework check for casts inside patterns.Gravatar Emilio Jesus Gallego Arias2017-05-15
| | | | * | | | | | | [interp] [ast] Make raw_cases_pattern_expr private.Gravatar Emilio Jesus Gallego Arias2017-05-15
| |_|_|/ / / / / / / |/| | | | | | | | |
| | | * | | | | | | Typo in comments of constrintern.Gravatar Hugo Herbelin2017-05-15
| | | | | * | | | | Removing a line warned unused.Gravatar Hugo Herbelin2017-05-14
| | | | | * | | | | Removing a variable warned unused.Gravatar Hugo Herbelin2017-05-14
| * | | | | | | | | [travis] Update OCaml to 4.04.1Gravatar Emilio Jesus Gallego Arias2017-05-13
| * | | | | | | | | [travis] Move VST to required suite.Gravatar Emilio Jesus Gallego Arias2017-05-13
|/ / / / / / / / /
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 05:39:15 +0000