aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Merge PR#705: Fix bug #5019 (looping zify on dependent types)Gravatar Maxime Dénès2017-06-02
|\
* \ Merge PR#631: Fix bug #5255Gravatar Maxime Dénès2017-06-01
|\ \
| | * Fix bug #5019 (looping zify on dependent types)Gravatar Jason Gross2017-06-01
| | * Add opened bug 5019Gravatar Jason Gross2017-06-01
* | | Merge PR#710: Add test-suite checks for coqchk with constraintsGravatar Maxime Dénès2017-06-01
|\ \ \ | |_|/ |/| |
* | | Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake (...Gravatar Maxime Dénès2017-05-31
|\ \ \
* \ \ \ Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with secti...Gravatar Maxime Dénès2017-05-31
|\ \ \ \
| | | * | Add test-suite checks for coqchk with constraintsGravatar Jason Gross2017-05-30
| |_|/ / |/| | |
* | | | Merge PR#693: A subtle bug in tclWITHHOLES.Gravatar Maxime Dénès2017-05-30
|\ \ \ \
* \ \ \ \ Merge PR#695: Omega: fix bug #4132Gravatar Maxime Dénès2017-05-30
|\ \ \ \ \
| | | * | | Fix bug 5550: "typeclasses eauto with" does not work with section variables.Gravatar Théo Zimmermann2017-05-30
| |_|/ / / |/| | | |
| * | | | Omega: use "simpl" only on coefficents, not on atoms (fix #4132)Gravatar Pierre Letouzey2017-05-29
|/ / / /
* | | | Merge PR#685: Fix a bug in checkerGravatar Maxime Dénès2017-05-29
|\ \ \ \
* \ \ \ \ Merge PR#546: Fix for bug #4499 and other minor related bugsGravatar Maxime Dénès2017-05-29
|\ \ \ \ \
| | * | | | Fix a bug in checkerGravatar Amin Timany2017-05-28
| |/ / / / |/| | | |
| | * | | Fixing a subtle bug in tclWITHHOLES.Gravatar Hugo Herbelin2017-05-28
| |/ / / |/| | |
* | | | Merge PR#679: Bug 5546, qualify datatype constructors when needed in Show MatchGravatar Maxime Dénès2017-05-28
|\ \ \ \
* \ \ \ \ Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if prin...Gravatar Maxime Dénès2017-05-26
|\ \ \ \ \
* \ \ \ \ \ Merge PR#672: Add parsers-examples target to fiat-parsers ciGravatar Maxime Dénès2017-05-26
|\ \ \ \ \ \
| | | * | | | Bug 5546, qualify datatype constructors when neededGravatar Paul Steckler2017-05-25
* | | | | | | Merge PR#416: Fix the way setoid_rewrite handles bindings.Gravatar Maxime Dénès2017-05-25
|\ \ \ \ \ \ \ | |_|_|/ / / / |/| | | | | |
| | * | | | | Add parsers-examples target to fiat-parsers ciGravatar Jason Gross2017-05-23
| |/ / / / / |/| | | | |
| * | | | | Fix bindings handling of setoid_rewrite.Gravatar Cyprien Mangin2017-05-23
|/ / / / /
* | | | | Merge PR#653: Bug #5535, test for Show with -emacsGravatar Maxime Dénès2017-05-20
|\ \ \ \ \
* \ \ \ \ \ Merge PR#641: Fix bug #5486, don't reverse ids in tuplesGravatar Maxime Dénès2017-05-20
|\ \ \ \ \ \
| | * | | | | add test for Show with -emacs, bug 5535Gravatar Paul Steckler2017-05-19
| |/ / / / / |/| | | | |
| | * | | | Fixing bug #5526,allow nonlinear variables in Notation patternsGravatar Paul Steckler2017-05-17
| * | | | | fix swapping of ids in tuples, bug 5486Gravatar Paul Steckler2017-05-17
|/ / / / /
* | | | | Merge PR#635: Fixing #5522 (anomaly with free vars of pat)Gravatar Maxime Dénès2017-05-17
|\ \ \ \ \
| * | | | | Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters).Gravatar Hugo Herbelin2017-05-16
| * | | | | Fixing a bug with nested "as" clauses in "match".Gravatar Hugo Herbelin2017-05-16
* | | | | | Merge PR#624: Switch bedrock to mit-plv baseGravatar Maxime Dénès2017-05-16
|\ \ \ \ \ \ | |/ / / / / |/| | | | |
| | | | | * Fix #5255: [Context (x : T := y)] should mean [Let x := y].Gravatar Pierre-Marie Pédrot2017-05-15
| | | |_|/ | | |/| |
* | | | | Removing a line warned unused.Gravatar Hugo Herbelin2017-05-14
* | | | | Removing a variable warned unused.Gravatar Hugo Herbelin2017-05-14
| |/ / / |/| | |
| * | | Switch bedrock to mit-plv baseGravatar Jason Gross2017-05-10
|/ / /
* | | Merge PR#604: FIx bug #5300: Anomaly: Uncaught exception Not_found" in "Print...Gravatar Maxime Dénès2017-05-10
|\ \ \
* \ \ \ Merge PR#591: Add bmsherman/topology to the ciGravatar Maxime Dénès2017-05-09
|\ \ \ \
| * | | | Put .travis.yml in alphabetical orderGravatar Jason Gross2017-05-09
* | | | | Merge PR#609: Fix bug #3659: -time should understand multibyte encodings.Gravatar Maxime Dénès2017-05-09
|\ \ \ \ \
| * | | | | Fix bug #3659: -time should understand multibyte encodings.Gravatar Pierre-Marie Pédrot2017-05-05
|/ / / / /
| | * / / FIx bug #5300: uncaught exception in "Print Assumptions".Gravatar Cyprien Mangin2017-05-03
| |/ / / |/| | |
* | | | Merge PR#603: Fix outdated description in RefMan.Gravatar Maxime Dénès2017-05-03
|\ \ \ \
| * | | | Fix outdated description in RefMan.Gravatar Théo Zimmermann2017-05-03
|/ / / /
* | | | Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions with...Gravatar Maxime Dénès2017-05-02
|\ \ \ \
* \ \ \ \ Merge PR#589: remove unneeded -emacs flag in coq-prog-args in test-suite filesGravatar Maxime Dénès2017-05-02
|\ \ \ \ \
* \ \ \ \ \ Merge PR#599: Repairing `Set Rewriting Schemes`Gravatar Maxime Dénès2017-05-02
|\ \ \ \ \ \
* | | | | | | Avoiding registering files from _build_ci when not calling Makefile.ci.Gravatar Hugo Herbelin2017-05-02
| | | | * | | Add bmsherman/topology to the ciGravatar Jason Gross2017-05-01
| |_|_|/ / / |/| | | | |
| * | | | | Fixing Set Rewriting Schemes bugs introduced in v8.5.Gravatar Hugo Herbelin2017-05-01
|/ / / / /
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 02:02:48 +0000