Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Changing the order of the goals generated by unshelve. | 2015-12-15 | |
| | |||
* | Extraction: replace unused variable names by _ in funs and matchs (fix #2842) | 2015-12-15 | |
| | | | | | | | | | | | This is done via a unique pass which seems roughly linear in practice, even on big developments like CompCert. There's a List.nth in an env at each MLrel, that could be made logarithmic if necessary via Okasaki's skew list for instance. Another approach would be to keep names (as a form of documentation), but prefix them by _ to please OCaml's warnings. For now, let's be radical and use the _ pattern. | ||
* | Extraction: allow basic beta-reduction even through a MLmagic (fix #2795) | 2015-12-14 | |
| | | | | | | This fix only handles MLapp(MLmagic(MLlam...),...). Someday, we'll have to properly investigate the interaction between all the other optimizations and MLmagic. But well, at least this precise bug is fixed now. | ||
* | Fixing little bug of coq_makefile with unterminated comment. | 2015-12-14 | |
| | | | | | Force failing when reaching end of file with unterminated comment when parsing Make (project) file. | ||
* | extraction_impl.v: fix a typo | 2015-12-14 | |
| | |||
* | A test file for Extraction Implicit (including bugs #4243 and #4228) | 2015-12-14 | |
| | |||
* | Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2) | 2015-12-14 | |
| | | | | | | | | | | | In front of "let rec f x y = ... in f n m", if n is now an implicit argument, then the argument x of the inner fixpoint f is also considered as implicit. This optimization is rather ad-hoc, since we only handle MLapp(MLfix()) for now, and the implicit argument should be reused verbatim as argument. Note that it might happen that x cannot be implicit in f. But in this case we would have add an error message about n still occurring somewhere... At least this small heuristic was easy to add, and was sufficient to solve the part 2 of bug #4243. | ||
* | Fix \label which was meants to be \ref in doc of CIC terms. | 2015-12-14 | |
| | |||
* | Remove a mention of Set Virtual Machine in doc. | 2015-12-14 | |
| | |||
* | CoqIDE: add 'you need to restart CoqIDE after changing shortcuts' message | 2015-12-14 | |
| | |||
* | Updating CHANGES with an incompatibility. | 2015-12-14 | |
| | |||
* | Revert PMP's fix of #2498, which introduces an incompatibility with lablgtk | 2015-12-14 | |
| | | | | | | | | | | | 2.14. Debian ships with lablgtk 2.16 only since a few months, so we apply the fix to trunk instead. This reverts commits: 490160d25d3caac1d2ea5beebbbebc959b1b3832. ef8718a7fd3bcd960d954093d8c636525e6cc492. 6f9cc3aca5bb0e5684268a7283796a9272ed5f9d. 901a9b29adf507370732aeafbfea6718c1842f1b. | ||
* | Flag -compat 8.4 now loads Coq.Compat.Coq84. | 2015-12-14 | |
| | |||
* | Moved proof_admitted to its own file, named "AdmitAxiom.v". | 2015-12-14 | |
| | |||
* | Test file for #4363 was not complete. | 2015-12-14 | |
| | |||
* | Extraction: cosmetically avoid generating spaces on empty lines | 2015-12-14 | |
| | |||
* | Extraction: also get rid of explicit '\n' for haskell | 2015-12-14 | |
| | |||
* | Extraction: fix a pretty-print issue | 2015-12-14 | |
| | | | | | Some explicit '\n' in Pp.str were interacting badly with Format boxes in Compcert, leading to right-flushed "sig..end" blocks in some .mli | ||
* | Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty phrase") | 2015-12-14 | |
| | |||
* | Extraction: documentation of the new option Unset Extraction SafeImplicits | 2015-12-12 | |
| | |||
* | Extraction: nicer implementation of Implicits | 2015-12-12 | |
| | | | | | | | | | | | | | | | | | | | Instead of the original hacks (embedding implicits in string msg in MLexn !) we now use a proper construction MLdummy (Kimplicit (r,i)) to replace the use of the i-th argument of constant or constructor r when this argument has been declared as implicit. A new option Set/Unset Extraction SafeImplicits controls what happens when some implicits still occur after an extraction : fail in safe mode, or otherwise produce some code nonetheless. This code is probably buggish if the implicits are actually used to do anything relevant (match, function call, etc), but it might also be fine if the implicits are just passed along. And anyway, this unsafe mode could help figure what's going on. Note: the MLdummy now expected a kill_reason, just as Tdummy. These kill_reason are now Ktype, Kprop (formerly Kother) and Kimplicit. Some minor refactoring on the fly. | ||
* | Extraction: check for remaining implicits after dead code removal (fix #4243) | 2015-12-12 | |
| | |||
* | Extraction: fix for bug #4334 (use of delta_resolver in Extract_env) | 2015-12-12 | |
| | | | | | | The ind_equiv field wasn't correctly set, due to some kernel names glitches (canonical vs. user). The fix is to take into account the delta_resolver while traversing module structures. | ||
* | Extraction: avoid generating some blanks at end-of-line | 2015-12-12 | |
| | |||
* | Indexing and documenting some options. | 2015-12-12 | |
| | |||
* | Optimize occur_evar_upto_types, avoiding repeateadly looking into the | 2015-12-11 | |
| | | | | same evar. | ||
* | Univs: Fix bug #4363, nested abstract. | 2015-12-11 | |
| | |||
* | Document removal of Set Virtual Machine and -vm in CHANGES. | 2015-12-11 | |
| | |||
* | Remove Set Virtual Machine from doc, since the command itself has been removed. | 2015-12-11 | |
| | |||
* | Add tactic native_cast_no_check, analog to vm_cast_no_check. | 2015-12-11 | |
| | |||
* | Fixing a pat%constr bug. Thanks to Enrico for reporting. | 2015-12-10 | |
| | |||
* | Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn. | 2015-12-10 | |
| | | | | Marking it as experimental. | ||
* | Fixing compilation with OCaml 3.12 after commit 9d45d45f3a87 on removing | 2015-12-10 | |
| | | | | "open Unix" from lib/system.ml. | ||
* | Silently ignore requests to _not_ clear something when that something cannot ↵ | 2015-12-10 | |
| | | | | | | be cleared. This should fix the contrib failures on tactics like "destruct (0)". | ||
* | Refman, ch. 4: A few fixes. | 2015-12-10 | |
| | |||
* | ENH: redundant examples were removed | 2015-12-10 | |
| | |||
* | FIX: wrong reference to a figure | 2015-12-10 | |
| | |||
* | CLEANUP: putting examples inside "figure" environment | 2015-12-10 | |
| | |||
* | ENH: The definition of the "_ ; _" operation on local context was added. | 2015-12-10 | |
| | |||
* | TYPOGRAPHY: adjustments | 2015-12-10 | |
| | |||
* | PROPOSITION: the side-condition was made more specific. | 2015-12-10 | |
| | |||
* | PROPOSITION: rephrasing of the explanation of the meaning of '[I:A|B]' | 2015-12-10 | |
| | |||
* | PROPOSITION: Added an explicit definition of the notation for enriching the ↵ | 2015-12-10 | |
| | | | | global environment (we use throughout the document) | ||
* | PROPOSITION: Added "if" and "then" words missing in the original sentence. | 2015-12-10 | |
| | |||
* | PROPOSITION: Example was simplified | 2015-12-10 | |
| | |||
* | DONE | 2015-12-10 | |
| | |||
* | COMMENT: question | 2015-12-10 | |
| | |||
* | COMMENT: question | 2015-12-10 | |
| | |||
* | COMMENT: question | 2015-12-10 | |
| | |||
* | COMMENT: question | 2015-12-10 | |
| |