aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-05-01Fixing Set Rewriting Schemes bugs introduced in v8.5.Hugo Herbelin
2017-05-01More consistent writing of de Bruijn.Théo Zimmermann
2017-05-01remove unneeded -emacs flag to coq-prog-argsPaul Steckler
2017-05-01Removing dead code in Autorewrite.Pierre-Marie Pédrot
2017-05-01Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Hugo Herbelin
2017-05-01Really fixing #2602 which was wrongly working because of #5487 hiding the cause.Hugo Herbelin
2017-05-01Fix for bug 5507. Mispelt de Bruijn.Théo Zimmermann
2017-05-01Avoiding registering files from _build_ci when not calling Makefile.ci.Hugo Herbelin
2017-05-01Answer to db28e827d: I did test the commit on test-suite but for someHugo Herbelin
2017-04-30Functional choice <-> [inhabited] and [forall] commuteGaetan Gilbert
2017-04-30Fix bug #5501: Universe polymorphism breaks proof involving auto.Pierre-Marie Pédrot
2017-04-30Fixing "decide equality"'s bug #5449.Hugo Herbelin
2017-04-29Suppress warning message in stdlib.Guillaume Melquiond
2017-04-28Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."Maxime Dénès
2017-04-28Revert "Renaming allow_patvar flag of intern_gen into pattern_mode."Maxime Dénès
2017-04-28Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"."Maxime Dénès
2017-04-28Allow interactive editing of {C,}Morphisms in PGJason Gross
2017-04-28Add .dir-locals.el and _CoqProject files for emacs stdlib editingJason Gross
2017-04-28Using a more explicit algebraic type for evars of kind "MatchingVar".Hugo Herbelin
2017-04-28Renaming allow_patvar flag of intern_gen into pattern_mode.Hugo Herbelin
2017-04-28Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Hugo Herbelin
2017-04-28Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Maxime Dénès
2017-04-27Post-rebase warnings (unused opens and 2 unused values)Gaetan Gilbert
2017-04-27Enable more warnings, and add -warn-error configure flagGaetan Gilbert
2017-04-27Fix 4.04 warningsGaetan Gilbert
2017-04-27Remove uses of [Flags.make_silent]Gaetan Gilbert
2017-04-27Warning 29: non escaped end of line may be non portableGaetan Gilbert
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-27Micromega: do not use Filename.temp_dir_path, remove unused valuesGaetan Gilbert
2017-04-27Remove unused constructorsGaetan Gilbert
2017-04-27Add [_] prefix to unused values which maybe should be keptGaetan Gilbert
2017-04-27Remove some unused values and typesGaetan Gilbert
2017-04-27Rename Sos_lib.(||) -> parser_or to avoid (deprecated) Pervasives.orGaetan Gilbert
2017-04-27Disambiguate Polynomial.Hyp and Mfourier.Hyp -> AssumGaetan Gilbert
2017-04-27Use [method!] to override methods (warning 7)Gaetan Gilbert
2017-04-27Fix omitted labels in function callsGaetan Gilbert
2017-04-27Remove unused [rec] keywordsGaetan Gilbert
2017-04-27Locally disable some warnings.Gaetan Gilbert
2017-04-27Merge PR#414: Some more theory on powerRZ.Maxime Dénès
2017-04-27Merge PR#583: [toplevel] More work on error handling.Maxime Dénès
2017-04-27Merge PR#587: Fix description of command-line arguments for Add (Rec) LoadPathMaxime Dénès
2017-04-27fix order of command-line arguments mentioned in Add LoadPathPaul Steckler
2017-04-27Merge PR#586: trivial cleanup commits which does not change Coq APIMaxime Dénès
2017-04-27Test for bug #5193: Uncaught exception Class_tactics.Search.ReachedLimitEx.Pierre-Marie Pédrot
2017-04-27Merge PR#568: Remove tactic compatibility layerMaxime Dénès
2017-04-27Tentative note in CHANGES about now applying βι while typing "match" branches.Hugo Herbelin
2017-04-27Test surgical use of beta-iota in the type of variables coming fromHugo Herbelin
2017-04-27A refined solution to the beta-iota discrepancies between 8.4 and 8.5 "refine".Hugo Herbelin
2017-04-27Document the API changes.Pierre-Marie Pédrot
2017-04-27Merge PR#584: Give andb_prop a simpler proofMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 23:48:09 +0000