| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-07-16 | Fixing a collision about the meta-variable ".." in recursive notations. | Hugo Herbelin | |
| This happens when recursive notations are used to define recursive notations. | |||
| 2016-07-13 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-07-13 | Fixing printing of evar name in an error message of instantiate. | Hugo Herbelin | |
| 2016-07-13 | Typo. | Hugo Herbelin | |
| 2016-07-13 | Makefile.dev: fix a typo in the 'logic' rule | Pierre Letouzey | |
| 2016-07-12 | Makefile.build: follow-up of commits by Matej on VERBOSE and READABLE_ML4 | Pierre Letouzey | |
| - With the ?= construction, we avoid warnings about undefined variables, while tolerating both 'make VERBOSE=1' and 'VERBOSE=1 make' - Some extra documentation and cleanup | |||
| 2016-07-12 | .gitignore: no more generated grammar/*.ml files | Pierre Letouzey | |
| 2016-07-12 | Makefile: no more .ml4.d hence no more rule to clean them | Pierre Letouzey | |
| 2016-07-12 | ".gitignore" update | Matej Kosik | |
| 2016-07-12 | removing ocamldoc-related syntax errors | Matej Kosik | |
| 2016-07-12 | expanding "make help" a little bit | Matej Kosik | |
| 2016-07-12 | Removing "READABLE_ML4=" from "Makefile.build" | Matej Kosik | |
| 2016-07-11 | Removing "VERBOSE=" from "Makefile.build" | Matej Kosik | |
| 2016-07-08 | Fixing the printing of unknown locations by adding a newline. | Pierre-Marie Pédrot | |
| 2016-07-08 | Adding a breaking space in warning names. | Pierre-Marie Pédrot | |
| 2016-07-08 | Remove spurious warnings about projections when requiring modules. | Pierre-Marie Pédrot | |
| 2016-07-08 | Add a few fixes in CHANGES that were forgotten. | Maxime Dénès | |
| We should really automate the generation of the log of fixes for CHANGES. | |||
| 2016-07-08 | Fix test file for #4858. | Maxime Dénès | |
| 2016-07-08 | Fixing #4906 (regression in printing an error message). | Hugo Herbelin | |
| 2016-07-08 | Typo in a comment of stdlib. | Hugo Herbelin | |
| 2016-07-08 | Update csdp.cache. | Maxime Dénès | |
| 2016-07-08 | Test file for #4858. | Maxime Dénès | |
| 2016-07-08 | Add test file for #4880. | Maxime Dénès | |
| 2016-07-08 | Update COPYRIGHT. | Maxime Dénès | |
| 2016-07-08 | Merge remote-tracking branch 'github/pr/243' into v8.5 | Maxime Dénès | |
| Was PR#243: fixing nsatz | |||
| 2016-07-07 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-07-07 | Merge remote-tracking branch 'github/bug4653' into v8.6 | Matthieu Sozeau | |
| 2016-07-07 | Prevent "Load" from displaying all the intermediate subgoals. | Guillaume Melquiond | |
| Note that even "Load Verbose" is not supposed to display them. | |||
| 2016-07-07 | Do not display goals in -compile-verbose mode (bug #4841). | Guillaume Melquiond | |
| The -verbose family of options is only meant to echo sentences as they are processed. The patch below broke this, while fixing another issue. That other issue will be fixed in the next commit. Revert "Fixing "Load" without "Verbose" in coqtop, after vernac_com lost its" This reverts commit 2a28c677c3c205ff453b7b5903e4c22f4de2649b. | |||
| 2016-07-07 | Do not use implicit type info for (x := t) bindings | Matthieu Sozeau | |
| This maintains compatibility, it is debatable if we should use implicit type information for lets to allow for coercions to fire. (Problem found in math-comp). | |||
| 2016-07-07 | Merge remote-tracking branch 'github/bug4873' into v8.6 | Matthieu Sozeau | |
| 2016-07-07 | Program: fix #4873: transparency option not used | Matthieu Sozeau | |
| 2016-07-06 | Update csdp.cache. | Maxime Dénès | |
| 2016-07-06 | Fix typo in configure (noticed by Jason). | Maxime Dénès | |
| 2016-07-06 | Merge branch 'primproj' into v8.6 | Matthieu Sozeau | |
| 2016-07-06 | Fix reopened bug #3317. | Matthieu Sozeau | |
| 2016-07-06 | Fixed bug #4622. | Matthieu Sozeau | |
| 2016-07-06 | Disallow dependent case on prim records w/o eta | Matthieu Sozeau | |
| 2016-07-06 | Renaming to more generic has_dependent_elim test | Matthieu Sozeau | |
| 2016-07-06 | Move is_prim... to Inductiveops and correct Scheme | Matthieu Sozeau | |
| Now scheme will not try to build ill-typed dependent analyses on recursive records with primitive projections but report a proper error. Minor change of the API (adding one error case to recursion_scheme_error). | |||
| 2016-07-06 | primproj: warning and avoid error. | Matthieu Sozeau | |
| When defining a (co)recursive inductive with primitive projections on, which lacks eta-conversion and hence dependent elimination, build only the associated non-dependent elimination principles, and warn about this. Also make the printing of the status of an inductive w.r.t. projections and eta conversion explicit in Print and About. | |||
| 2016-07-06 | improved complexity in nsatz | thery | |
| we use a hashtable to reduce the complexity of creating a duplicate-free list. | |||
| 2016-07-06 | Merge remote-tracking branch 'github/pr/199' into v8.5 | Maxime Dénès | |
| Was PR#199: Unbreak singleton list-like notation (-compat 8.4) | |||
| 2016-07-06 | Merge remote-tracking branch 'github/pr/241' into v8.5 | Maxime Dénès | |
| Was PR#241: Restore option_map in FMapFacts | |||
| 2016-07-06 | Fix #4793: Coq 8.6 should accept -compat 8.6 | Maxime Dénès | |
| We also add a Coq86.v compat file. | |||
| 2016-07-06 | Bump version number in preparation for 8.5pl2 release. | Maxime Dénès | |
| 2016-07-06 | Fix test-suite file 3690 | Matthieu Sozeau | |
| 2016-07-06 | Deduplicate some names in .mailmap | Jason Gross | |
| 2016-07-06 | Univs: fix internalization of (x := T) and casts | Matthieu Sozeau | |
| They were allowing algebraic universes to slip in terms. | |||
| 2016-07-06 | Fix indentation of configure printout | Jason Gross | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |