aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Merge branch 'master' into ltac2-hooksGravatar Pierre-Marie Pédrot2017-05-19
|\
* | Adding a trespasser warning to the Nametab API.Gravatar Pierre-Marie Pédrot2017-05-18
| * Merge PR#633: An extension of EXTEND and notations to make standard parsing t...Gravatar Maxime Dénès2017-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
| |\ \ \
| * \ \ \ 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
| |/ / / / / / / /
| | | * | | | | | Uniformity of style for selecting plural or not; spacing for comma.Gravatar Hugo Herbelin2017-05-13
| | | * | | | | | Typo in a comment of plugin Quote.Gravatar Hugo Herbelin2017-05-13
| | | * | | | | | Aligning on standard layout of CHANGES.Gravatar Hugo Herbelin2017-05-13
| | |/ / / / / / | |/| | | | | |
| | * | | | | | Add documentation for Set Ltac Batch DebugGravatar Jason Gross2017-05-11
| |/ / / / / /
| | | | | | * Documenting Printing Compact Contexts + CHANGESGravatar Pierre Courtieu2017-05-11
| * | | | | | Merge PR#594: An example showing the benefit of EconstrGravatar Maxime Dénès2017-05-11
| |\ \ \ \ \ \
| * \ \ \ \ \ \ Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 a...Gravatar Maxime Dénès2017-05-11
| |\ \ \ \ \ \ \
| * \ \ \ \ \ \ \ Merge PR#572: Replacing costly merges in UGraph.Gravatar Maxime Dénès2017-05-11
| |\ \ \ \ \ \ \ \
| * | | | | | | | | Remove an unused open introduced by the previous commit.Gravatar Maxime Dénès2017-05-11
| * | | | | | | | | Merge PR#201: Transparent abstractGravatar Maxime Dénès2017-05-11
| |\ \ \ \ \ \ \ \ \
| | | | | | | | * | | Switch bedrock to mit-plv baseGravatar Jason Gross2017-05-10
| | | | | | | |/ / /
| | | | | | | * | | Merge PR#604: FIx bug #5300: Anomaly: Uncaught exception Not_found" in "Print...Gravatar Maxime Dénès2017-05-10
| | | | | | | |\ \ \
| | | | | | * | | | | Moving code for miscellaneous tests to specific files.Gravatar Hugo Herbelin2017-05-10
| | | | | | * | | | | A more regular naming of variables in test-suite Makefile.Gravatar Hugo Herbelin2017-05-10
| | | | | | * | | | | Adding tests for testing exit status and #use"include".Gravatar Hugo Herbelin2017-05-10
| | | | | | * | | | | Cleaning old untested not any more interesting testing files.Gravatar Hugo Herbelin2017-05-10
| | |_|_|_|/ / / / / | |/| | | | | | | |
| | | | | | * | | | Merge PR#591: Add bmsherman/topology to the ciGravatar Maxime Dénès2017-05-09
| | | | | | |\ \ \ \
| | | | | | | * | | | Put .travis.yml in alphabetical orderGravatar Jason Gross2017-05-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 20:45:47 +0000