| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-01-16 | Add two lemmas about firstn to the List standard library. | Sébastien Hinderer | |
| 2015-01-16 | Lemmas related to the firstn function over lists. | Sébastien Hinderer | |
| 2015-01-16 | ListSet: follow-up of Sebastien's last commit | Pierre Letouzey | |
| More results on set_remove, in particular explicit the NoDup pre-condition. Show that NoDup is preserved by other operations. | |||
| 2015-01-16 | Work in progress on listset. | Sébastien Hinderer | |
| 2015-01-16 | Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _" | Matthieu Sozeau | |
| Not supposed to be part of 8.5beta. This reverts commit 74682bb27da074fedc115238f3085baaccf12d73. | |||
| 2015-01-15 | Added stuff about -I -Q -R in COMPATIBILTY. | Pierre Courtieu | |
| 2015-01-15 | vm_printers: fix compilation | Enrico Tassi | |
| 2015-01-15 | Correct restriction of vm_compute when handling universe polymorphic | Matthieu Sozeau | |
| definitions. Instead of failing with an anomaly when trying to do conversion or computation with the vm's, consider polymorphic constants as being opaque and keep instances around. This way the code is still correct but (obviously) incomplete for polymorphic definitions and we avoid introducing an anomaly. The patch does nothing clever, it only keeps around instances with constants/inductives and compile constant bodies only for non-polymorphic definitions. | |||
| 2015-01-15 | Minor fixes to the refman credits to be continued. | Matthieu Sozeau | |
| 2015-01-15 | Move explanations about primitive projections to the manual. | Matthieu Sozeau | |
| 2015-01-15 | Add a (by default deactivated) option to force typeclass resolution to | Matthieu Sozeau | |
| respect dependencies between typeclass goals, trying to solve the least dependent ones first. | |||
| 2015-01-15 | Expand Credits for 8.5 and doc on universes | Matthieu Sozeau | |
| 2015-01-15 | Remove typeclass opaque directive, some proofs in the stdlib rely on it ↵ | Matthieu Sozeau | |
| being transparent | |||
| 2015-01-15 | Optionally allow eta-conversion during unification for type classes. | Matthieu Sozeau | |
| Off by default as it can be backwards-incompatible (e.g. produces loop in the library without an additional Typeclasses Opaque directive in RelationPairs). | |||
| 2015-01-15 | Update header of CHANGES. | Maxime Dénès | |
| 2015-01-15 | Revert "Bump version and magic numbers in configure." | Maxime Dénès | |
| This reverts commit 5f49780b395686cdfce7126438c6dd69712d5c70. | |||
| 2015-01-15 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| Conflicts: tools/coq_makefile.ml | |||
| 2015-01-15 | Remove left-over dead code in previous commit. | Maxime Dénès | |
| 2015-01-15 | Make -print-mod-uid accept a list of files. | Maxime Dénès | |
| Solves an efficiency problem in Makefiles generated by coq_makefile. | |||
| 2015-01-15 | Mention CHANGES file in COMPATIBILITY. | Maxime Dénès | |
| 2015-01-15 | Mention guard condition in CHANGES. | Maxime Dénès | |
| 2015-01-15 | Make installation of native files more robust. | Maxime Dénès | |
| 2015-01-15 | Mention CHANGES file in COMPATIBILITY. | Maxime Dénès | |
| 2015-01-15 | Mention guard condition in CHANGES. | Maxime Dénès | |
| 2015-01-15 | Make installation of native files more robust. | Maxime Dénès | |
| 2015-01-15 | Hugo put me in credits, but I was already there :) | Maxime Dénès | |
| 2015-01-15 | Makefile: install ide/*lang | Enrico Tassi | |
| 2015-01-15 | coq_makefile: chmod 755 on toplopp cmxs | Enrico Tassi | |
| 2015-01-15 | CoqIDE: a Make file to build coqidetop toploop | Enrico Tassi | |
| 2015-01-15 | coq_makefile installs native files | Pierre Boutillier | |
| 2015-01-15 | Always build (even when -coqide no) and install idetoploop | Pierre Boutillier | |
| So you can link a coqtop compiled (by opam) without coqide to a stand alone coqide (binary distributed) | |||
| 2015-01-15 | Hugo put me in credits, but I was already there :) | Maxime Dénès | |
| 2015-01-15 | Tentatively updating credits while remaining brief. | Hugo Herbelin | |
| 2015-01-14 | Makefile: install ide/*lang | Enrico Tassi | |
| 2015-01-14 | coq_makefile: chmod 755 on toplopp cmxs | Enrico Tassi | |
| 2015-01-14 | CoqIDE: a Make file to build coqidetop toploop | Enrico Tassi | |
| 2015-01-14 | Reference manual: I had previously omitted the syntax entry for [> t1|…|tn]. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: document tryif/then/else. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: document multimatch. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: try and improve documentation for Ltac's match. | Arnaud Spiwack | |
| In particular document the "once" behaviour. | |||
| 2015-01-14 | Reference manual: try and improve the documentation of lazymatch. | Arnaud Spiwack | |
| In particular try to avoid the use of the word "backtracking" which refers to too many things. | |||
| 2015-01-14 | Reference manual: document gfail. | Arnaud Spiwack | |
| 2015-01-14 | CHANGES: my recent updates to Ltac. | Arnaud Spiwack | |
| - gfail - multimatch - tryif/then/else | |||
| 2015-01-14 | Reference manual: I had previously omitted the syntax entry for [> t1|…|tn]. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: document tryif/then/else. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: document multimatch. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: try and improve documentation for Ltac's match. | Arnaud Spiwack | |
| In particular document the "once" behaviour. | |||
| 2015-01-14 | Reference manual: try and improve the documentation of lazymatch. | Arnaud Spiwack | |
| In particular try to avoid the use of the word "backtracking" which refers to too many things. | |||
| 2015-01-14 | Reference manual: document gfail. | Arnaud Spiwack | |
| 2015-01-14 | CHANGES: my recent updates to Ltac. | Arnaud Spiwack | |
| - gfail - multimatch - tryif/then/else | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |