aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-05-17Merge PR#607: Make congruence reuse discriminate instead of rolling its own.Maxime Dénès
2017-05-17Merge branch 'v8.6'Pierre-Marie Pédrot
2017-05-17Merge PR#620: Reorganization of the layout for miscellaneous testsMaxime Dénès
2017-05-17Merge PR#614: Improve TravisMaxime Dénès
2017-05-17Travis: add -warn-error targets (standard and 4.04.1 ocaml)Gaetan Gilbert
2017-05-17Merge PR#630: [interp] [ast] Make raw_cases_pattern_expr private + small cleanupMaxime Dénès
2017-05-17Travis: deduplicate package list for coqide+documentation targetsGaetan Gilbert
2017-05-17Travis: do not run the tests if building Coq failsGaetan Gilbert
2017-05-17Merge PR#635: Fixing #5522 (anomaly with free vars of pat)Maxime Dénès
2017-05-17Merge PR#636: Miscellaneous typos, dead code, etc.Maxime Dénès
2017-05-17Merge PR#639: Stop using auto with * in two proofs.Maxime Dénès
2017-05-16Stop using auto with * in two proofs.Théo Zimmermann
2017-05-16Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters).Hugo Herbelin
2017-05-16Fixing a bug with nested "as" clauses in "match".Hugo Herbelin
2017-05-16Merge PR#624: Switch bedrock to mit-plv baseMaxime Dénès
2017-05-16Merge PR#626: Add documentation for Set Ltac Batch DebugMaxime Dénès
2017-05-16Merge PR#629: A couple of simple updates for TravisMaxime Dénès
2017-05-15Dead code in coqdep.Hugo Herbelin
2017-05-15[interp] Rework check for casts inside patterns.Emilio Jesus Gallego Arias
2017-05-15[interp] [ast] Make raw_cases_pattern_expr private.Emilio Jesus Gallego Arias
2017-05-15Typo in comments of constrintern.Hugo Herbelin
2017-05-14Removing a line warned unused.Hugo Herbelin
2017-05-14Removing a variable warned unused.Hugo Herbelin
2017-05-13[travis] Update OCaml to 4.04.1Emilio Jesus Gallego Arias
2017-05-13[travis] Move VST to required suite.Emilio Jesus Gallego Arias
2017-05-13Uniformity of style for selecting plural or not; spacing for comma.Hugo Herbelin
2017-05-13Typo in a comment of plugin Quote.Hugo Herbelin
2017-05-13Aligning on standard layout of CHANGES.Hugo Herbelin
2017-05-11Add documentation for Set Ltac Batch DebugJason Gross
2017-05-11Merge PR#594: An example showing the benefit of EconstrMaxime Dénès
2017-05-11Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 a...Maxime Dénès
2017-05-11Merge PR#572: Replacing costly merges in UGraph.Maxime Dénès
2017-05-11Remove an unused open introduced by the previous commit.Maxime Dénès
2017-05-11Merge PR#201: Transparent abstractMaxime Dénès
2017-05-10Switch bedrock to mit-plv baseJason Gross
2017-05-10Merge PR#604: FIx bug #5300: Anomaly: Uncaught exception Not_found" in "Print...Maxime Dénès
2017-05-10Moving code for miscellaneous tests to specific files.Hugo Herbelin
2017-05-10A more regular naming of variables in test-suite Makefile.Hugo Herbelin
2017-05-10Adding tests for testing exit status and #use"include".Hugo Herbelin
2017-05-10Cleaning old untested not any more interesting testing files.Hugo Herbelin
2017-05-09Merge PR#591: Add bmsherman/topology to the ciMaxime Dénès
2017-05-09Put .travis.yml in alphabetical orderJason Gross
2017-05-09Merge PR#619: Fix warnings in top_printersMaxime Dénès
2017-05-09Merge PR#612: Set Ltac Batch DebugMaxime Dénès
2017-05-09Merge PR#606: Added an option Set Debug CbvMaxime Dénès
2017-05-09Merge PR#621: Prevent user-defined ring morphisms from ever being evaluated.Maxime Dénès
2017-05-09Merge PR#615: coqtop -help: don't die if coqlib can't be foundMaxime Dénès
2017-05-09Merge PR#609: Fix bug #3659: -time should understand multibyte encodings.Maxime Dénès
2017-05-09Merge PR#617: [toplevel] Fix a couple of logical errors in error printing.Maxime Dénès
2017-05-09Prevent user-defined ring morphisms from ever being evaluated.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-05 03:31:53 +0000