| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| | | * | | | | | | | | | | Moving UTF-8 related functions to Unicode module. |  Pierre-Marie Pédrot | 2016-06-14 | |
| | | * | | | | | | | | | | Revert "Strip some trailing spaces" | Pierre-Marie Pédrot | 2016-06-13 | |
| * | | | | | | | | | | | | Univs: more robust Universe/Constraint decls #4816 |  Matthieu Sozeau | 2016-06-13 | |
| * | | | | | | | | | | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-06-13 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | * | | | | | | | STM classification: VernacTimeout may contain an "internal command". |  Maxime Dénès | 2016-06-13 | |
| | | | | | | * | | | | | | | Print Assumptions and co. can "pierce opacity". | Maxime Dénès | 2016-06-13 | |
| | |_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | ||||
| | * | | | | | | | | | | | evar_conv: Refine occur_rigidly |  Matthieu Sozeau | 2016-06-13 | |
| | * | | | | | | | | | | | Tentatively fixing misguiding error message with "binder" type in |  Hugo Herbelin | 2016-06-13 | |
| * | | | | | | | | | | | | For the record, an example one would like to see working. | Hugo Herbelin | 2016-06-12 | |
| | * | | | | | | | | | | | Minor simplification in evarconv. | Hugo Herbelin | 2016-06-12 | |
| | * | | | | | | | | | | | Another fix to #4782 (a typing error not captured when dealing with bindings). | Hugo Herbelin | 2016-06-12 | |
| | * | | | | | | | | | | | Reserve exception "ConversionFailed" in unification for failure of | Hugo Herbelin | 2016-06-12 | |
| | * | | | | | | | | | | | Protecting eta-expansion in evarconv.ml against ill-typed problems. | Hugo Herbelin | 2016-06-12 | |
| | * | | | | | | | | | | | Fixing bug in printing CannotSolveConstraint (collision of context names). | Hugo Herbelin | 2016-06-12 | |
| | * | | | | | | | | | | | Fixing #4782 (a typing error not captured when dealing with bindings). | Hugo Herbelin | 2016-06-11 | |
| | * | | | | | | | | | | | Fixing a try with in apply that has become too weak in 8.5. | Hugo Herbelin | 2016-06-11 | |
| * | | | | | | | | | | | | Merge branch 'pack-plugins' |  Pierre Letouzey | 2016-06-10 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | | | | | coq_makefile: oups, a missing ; in my previous commit | Pierre Letouzey | 2016-06-10 | |
| | * | | | | | | | | | | | | coq_makefile: fix a crucial typo in e9c57a3 | Pierre Letouzey | 2016-06-10 | |
| * | | | | | | | | | | | | | coq_makefile: short display of COQC and COQDEP (follow-up of e9c57a3) | Pierre Letouzey | 2016-06-10 | |
| * | | | | | | | | | | | | | A mini-optimization for free in unification.ml: test in O(1) | Hugo Herbelin | 2016-06-10 | |
| | | * | | | | | | | | | | | Reporting about a few bug fixes (to be continued). | Hugo Herbelin | 2016-06-09 | |
| | | | * | | | | | | | | | | newring: fix for hack using evars as integers. | Matthieu Sozeau | 2016-06-09 | |
| | |_|/ / / / / / / / / / |/| | | | | | | | | | | | ||||
| * | | | | | | | | | | | | Adding a bit of documentation in the mli. | Pierre-Marie Pédrot | 2016-06-09 | |
| * | | | | | | | | | | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-06-09 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | | |/ / / / / / / / / / | |/| | | | | | | | | | | ||||
| | * | | | | | | | | | | | Fixing #4644 (regression of unification on evar-evar problems with a match). | Hugo Herbelin | 2016-06-09 | |
| | * | | | | | | | | | | | Minor simplification in evarconv.ml. | Hugo Herbelin | 2016-06-09 | |
| | * | | | | | | | | | | | New update on how to find camlp5 binary and library at configure time. | Hugo Herbelin | 2016-06-09 | |
| | * | | | | | | | | | | | Improve the interpretation scope of arguments of an ltac match. | Hugo Herbelin | 2016-06-09 | |
| | * | | | | | | | | | | | Reverting dbdff037 which does not seem to prevent to have #3638 fixed | Hugo Herbelin | 2016-06-09 | |
| * | | | | | | | | | | | | Documenting API changes in dev/doc/changes.txt. | Pierre-Marie Pédrot | 2016-06-09 | |
| * | | | | | | | | | | | | Merge PR #190: Add configurable shortcuts for user queries to CoqIDE. | Pierre-Marie Pédrot | 2016-06-09 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #197. | Pierre-Marie Pédrot | 2016-06-09 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | * | | | | | | | | | | | Remove failure on non-.v files (bug #4752). |  Guillaume Melquiond | 2016-06-09 | |
| * | | | | | | | | | | | | | | Adding profiling developer information in dev/doc/profiling.txt. | Pierre-Marie Pédrot | 2016-06-08 | |
| | * | | | | | | | | | | | | | Add an explicit replacement rule for Refine module |  Jason Gross | 2016-06-08 | |
| |/ / / / / / / / / / / / / | ||||
| * | | | | | | | | | | | | | coq_makefile: fix a crucial typo in e9c57a3 | Pierre Letouzey | 2016-06-08 | |
| * | | | | | | | | | | | | | remove grammar/grammar.mllib | Pierre Letouzey | 2016-06-08 | |
| | | | * | | | | | | | | | | Compilation via pack for plugins of the stdlib | Pierre Letouzey | 2016-06-08 | |
| | |_|/ / / / / / / / / / |/| | | | | | | | | | | | ||||
| * | | | | | | | | | | | | Merge branch 'divided-makefile' into trunk | Pierre Letouzey | 2016-06-08 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | | | | Makefile.build split in many smaller files : Makefile.{ide,checker,dev,install} | Pierre Letouzey | 2016-06-08 | |
| | * | | | | | | | | | | | | Makefile: avoid overwriting test.ml when testing grammar.cma | Pierre Letouzey | 2016-06-08 | |
| | * | | | | | | | | | | | | Makefile: make clean now removes the .coq-native subdirs | Pierre Letouzey | 2016-06-08 | |
| |/ / / / / / / / / / / / | ||||
| * | | | | | | | | | | | | Officially discontinue the experimental coq build via ocamlbuild | Pierre Letouzey | 2016-06-08 | |
| * | | | | | | | | | | | | proofs/proofs.mllib: no more proof_errors ! | Pierre Letouzey | 2016-06-08 | |
| | | | | | | | | | | | * | Add is_ind, is_constructor, is_proj |  Jason Gross | 2016-06-07 | |
| | |_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | ||||
| * | | | | | | | | | | | Search interface revisions. | Pierre-Marie Pédrot | 2016-06-07 | |
| |\ \ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | | | Removing the convenience functions from the Search API. | Pierre-Marie Pédrot | 2016-06-07 | |
| | | | * | | | | | | | | | Fix bug #4777: Printing time is impacted by large terms that don't print. | Pierre-Marie Pédrot | 2016-06-07 | |
| | | | | | * | | | | | | | CoqIDE: remove useless print |  Enrico Tassi | 2016-06-07 | |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |