aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2017-05-08Fix warnings in top_printersGaetan Gilbert
2017-05-05[toplevel] Fix a couple of logical errors in error printing.Emilio Jesus Gallego Arias
2017-05-05Remove dead code and unused open.Maxime Dénès
2017-05-05Merge PR#558: Adding a fold_glob_constr_with_binders combinatorMaxime Dénès
2017-05-05Remove two unused opens.Maxime Dénès
2017-05-05Merge PR#598: Removing dead code in Autorewrite.Maxime Dénès
2017-05-05Fix bug #3659: -time should understand multibyte encodings.Pierre-Marie Pédrot
2017-05-05Documenting Option.List.find.Hugo Herbelin
2017-05-05Cosmetic: unifying style within option.ml.Hugo Herbelin
2017-05-05Upgrading some local function as a general-purpose combinator Option.List.map.Hugo Herbelin
2017-05-05Adding a test-suite pattern-unification example that Econstr fixed.Hugo Herbelin
2017-05-05Merge PR#610: Improve documentation of assert / pose proof / specialize.Maxime Dénès
2017-05-05Merge PR#605: Report a useful error for dependent inductionMaxime Dénès
2017-05-05coqtop -help: don't die if coqlib can't be foundGaetan Gilbert
2017-05-05Merge PR#454: Printing unfocussed goals and toward a pg plugin.Maxime Dénès
2017-05-05Merge PR#593: Functional choice <-> [inhabited] and [forall] commuteMaxime Dénès
2017-05-05Remove unused open.Maxime Dénès
2017-05-05Merge PR#544: Anonymous universesMaxime Dénès
2017-05-05Adapted to EConstr.Pierre Courtieu
2017-05-04Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in bat...Hugo Herbelin
2017-05-04Improve documentation of assert / pose proof / specialize.Théo Zimmermann
2017-05-04Warning removed.Pierre Courtieu
2017-05-04labelizing argumentsPierre Courtieu
2017-05-04Adding an option "Printing Unfocused".Pierre Courtieu
2017-05-03FIx bug #5300: uncaught exception in "Print Assumptions".Cyprien Mangin
2017-05-03Merge PR#541: Fixing "decide equality" bug #5449Maxime Dénès
2017-05-03Merge PR#588: Allow interactive editing of {C,}Morphisms in PGMaxime Dénès
2017-05-03Merge PR#386: Better editing of the standard library in coqtop/PGMaxime Dénès
2017-05-03Make congruence reuse discriminate instead of rolling its own.Gaetan Gilbert
2017-05-03Merge PR#602: Fix more warningsMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 22:51:43 +0000