aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-06-04configure: avoid deprecated warningsPierre Letouzey
2017-06-02Merge PR#705: Fix bug #5019 (looping zify on dependent types)Maxime Dénès
2017-06-01Merge PR#631: Fix bug #5255Maxime Dénès
2017-06-01Fix bug #5019 (looping zify on dependent types)Jason Gross
2017-06-01Add opened bug 5019Jason Gross
2017-06-01Merge PR#710: Add test-suite checks for coqchk with constraintsMaxime Dénès
2017-05-31Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake (...Maxime Dénès
2017-05-31Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with secti...Maxime Dénès
2017-05-30Add test-suite checks for coqchk with constraintsJason Gross
2017-05-30Merge PR#693: A subtle bug in tclWITHHOLES.Maxime Dénès
2017-05-30Merge PR#695: Omega: fix bug #4132Maxime Dénès
2017-05-30Fix bug 5550: "typeclasses eauto with" does not work with section variables.Théo Zimmermann
2017-05-29Omega: use "simpl" only on coefficents, not on atoms (fix #4132)Pierre Letouzey
2017-05-29Merge PR#685: Fix a bug in checkerMaxime Dénès
2017-05-29Merge PR#546: Fix for bug #4499 and other minor related bugsMaxime Dénès
2017-05-28Fix a bug in checkerAmin Timany
2017-05-28Fixing a subtle bug in tclWITHHOLES.Hugo Herbelin
2017-05-28Merge PR#679: Bug 5546, qualify datatype constructors when needed in Show MatchMaxime Dénès
2017-05-26Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if prin...Maxime Dénès
2017-05-26Merge PR#672: Add parsers-examples target to fiat-parsers ciMaxime Dénès
2017-05-25Bug 5546, qualify datatype constructors when neededPaul Steckler
2017-05-25Merge PR#416: Fix the way setoid_rewrite handles bindings.Maxime Dénès
2017-05-23Add parsers-examples target to fiat-parsers ciJason Gross
2017-05-23Fix bindings handling of setoid_rewrite.Cyprien Mangin
2017-05-20Merge PR#653: Bug #5535, test for Show with -emacsMaxime Dénès
2017-05-20Merge PR#641: Fix bug #5486, don't reverse ids in tuplesMaxime Dénès
2017-05-19add test for Show with -emacs, bug 5535Paul Steckler
2017-05-17Fixing bug #5526,allow nonlinear variables in Notation patternsPaul Steckler
2017-05-17fix swapping of ids in tuples, bug 5486Paul Steckler
2017-05-17Merge PR#635: Fixing #5522 (anomaly with free vars of pat)Maxime Dénès
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-15Fix #5255: [Context (x : T := y)] should mean [Let x := y].Pierre-Marie Pédrot
2017-05-14Removing a line warned unused.Hugo Herbelin
2017-05-14Removing a variable warned unused.Hugo Herbelin
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-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#609: Fix bug #3659: -time should understand multibyte encodings.Maxime Dénès
2017-05-05Fix bug #3659: -time should understand multibyte encodings.Pierre-Marie Pédrot
2017-05-03FIx bug #5300: uncaught exception in "Print Assumptions".Cyprien Mangin
2017-05-03Merge PR#603: Fix outdated description in RefMan.Maxime Dénès
2017-05-03Fix outdated description in RefMan.Théo Zimmermann
2017-05-02Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions with...Maxime Dénès
2017-05-02Merge PR#589: remove unneeded -emacs flag in coq-prog-args in test-suite filesMaxime Dénès
2017-05-02Merge PR#599: Repairing `Set Rewriting Schemes`Maxime Dénès
2017-05-02Avoiding registering files from _build_ci when not calling Makefile.ci.Hugo Herbelin
2017-05-01Add bmsherman/topology to the ciJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 22:31:05 +0000