aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-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-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
2017-05-01Fixing Set Rewriting Schemes bugs introduced in v8.5.Hugo Herbelin
2017-05-01remove unneeded -emacs flag to coq-prog-argsPaul Steckler
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-01Answer to db28e827d: I did test the commit on test-suite but for someHugo Herbelin
2017-04-28Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."Maxime Dénès
2017-04-28Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Hugo Herbelin
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-27Test for bug #5193: Uncaught exception Class_tactics.Search.ReachedLimitEx.Pierre-Marie Pédrot
2017-04-25Fix an optimization failure in tclPROGRESS.Pierre-Marie Pédrot
2017-04-25Merge PR#567: Fix bug #5377: @? patterns broken.Maxime Dénès
2017-04-24Merge PR#577: Add bedrock targets src and facade to Travis CIMaxime Dénès
2017-04-20Add bedrock targets src and facadeJason Gross
2017-04-20Fix bug #5377: @? patterns broken.Pierre-Marie Pédrot
2017-04-19Merge PR#538: Correction of bug #4306Maxime Dénès
2017-04-14Fixing bug #5470 (anomaly on notations with misused "binder" type).Hugo Herbelin
2017-04-14Fixing bug #5469 (notation format not recognizing curly braces).Hugo Herbelin
2017-04-14Fix EOL characters in xml protocol documentation.Maxime Dénès
2017-04-14Merge PR#556: Fix anomaly when doing [all:Check _.] during a proof.Maxime Dénès