| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-15 | Proof using: do not clear unused section hyps automatically | Enrico Tassi | |
| The option is still there, but not documented since it is too dangerous. Hints and type classes instances are not taking cleared variables into account. | |||
| 2015-12-15 | Fix test suite after change in extraction. | Maxime Dénès | |
| 2015-12-15 | Extraction: more cautious use of intermediate result caching (fix #3923) | Pierre Letouzey | |
| During an extraction, a few tables are maintained to cache intermediate results. Due to modules, the kernel_name index for these caching tables aren't enough. For instance, in bug #3923, a constant is first transparent (from inside the module) then opaque (when seen from the signature). The previous protections were actually obsolete (tests via visible_con), we now checks that the constant_body is still the same. | |||
| 2015-12-15 | Fix test-suite files after change in refine tactic. | Maxime Dénès | |
| Change was introduced by cedcfc9bc386456f3fdd225f739706e4f7a2902c. | |||
| 2015-12-15 | Extraction: fix a few little glitches with my last commit (replacing unused ↵ | Pierre Letouzey | |
| vars by _) | |||
| 2015-12-15 | Fixing e3cefca41b about supposingly simplifying primitive projections | Hugo Herbelin | |
| typing. Had built the instance for substitution in the wrong context. | |||
| 2015-12-15 | Fixing unexpected length of context in a typing function, detected by | Hugo Herbelin | |
| cleaning done in e8c47b652a0. It had no serious consequences except having whd-reduction blocked on a let-in when typing a return clause with let-ins in the arity (a priori resulting in return types of the form e.g. "(let x:=t in fun y => T) u" instead of T[x:=t;y:=u], if I'm not mistaking). This fixes 3210.v in test-suite. | |||
| 2015-12-15 | Adding a test for the unshelve tactical. | Pierre-Marie Pédrot | |
| 2015-12-15 | Refine tactic now shelves unifiable holes. | Pierre-Marie Pédrot | |
| The unshelve tactical can be used to get the shelved holes. This changes the proper ordering of holes though, so expect some broken scripts. Also, the test-suite is not fixed yet. | |||
| 2015-12-15 | Fixing e7f7fc3e058 (wrong chop on contexts). This fixes test-suite. | Hugo Herbelin | |
| 2015-12-15 | API: documenting context_chop and removing a duplicate. | Hugo Herbelin | |
| 2015-12-15 | Changing the order of the goals generated by unshelve. | Pierre-Marie Pédrot | |
| 2015-12-15 | Adding a token "index" representing positions (1st, 2nd, etc.). | Hugo Herbelin | |
| 2015-12-15 | Simplifying documentation of "assert form as pat". | Hugo Herbelin | |
| 2015-12-15 | Granting clear_flag in injection, even legacy mode. This is possible | Hugo Herbelin | |
| since the clear_flag is new. | |||
| 2015-12-15 | Tactics: Generalizing the use of the experimental clearing modifier to | Hugo Herbelin | |
| all cases of rewrite. | |||
| 2015-12-15 | Extraction: replace unused variable names by _ in funs and matchs (fix #2842) | Pierre Letouzey | |
| 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. | |||
| 2015-12-15 | Revert "Revert PMP's fix of #2498, which introduces an incompatibility with ↵ | Pierre-Marie Pédrot | |
| lablgtk" This reverts commit 469cb750c6c1aa46f77b2a89a36f79f29aa97073. | |||
| 2015-12-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-14 | Extraction: allow basic beta-reduction even through a MLmagic (fix #2795) | Pierre Letouzey | |
| 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. | |||
| 2015-12-14 | Fixing little bug of coq_makefile with unterminated comment. | Hugo Herbelin | |
| Force failing when reaching end of file with unterminated comment when parsing Make (project) file. | |||
| 2015-12-14 | extraction_impl.v: fix a typo | Pierre Letouzey | |
| 2015-12-14 | A test file for Extraction Implicit (including bugs #4243 and #4228) | Pierre Letouzey | |
| 2015-12-14 | Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2) | Pierre Letouzey | |
| 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. | |||
| 2015-12-14 | Adding compatibility flag for 8.5. | Hugo Herbelin | |
| Soon needing a more algebraic view at version numbers... | |||
| 2015-12-14 | Fix \label which was meants to be \ref in doc of CIC terms. | Maxime Dénès | |
| 2015-12-14 | Remove a mention of Set Virtual Machine in doc. | Maxime Dénès | |
| 2015-12-14 | CoqIDE: add 'you need to restart CoqIDE after changing shortcuts' message | Enrico Tassi | |
| 2015-12-14 | Updating CHANGES with an incompatibility. | Hugo Herbelin | |
| 2015-12-14 | Revert PMP's fix of #2498, which introduces an incompatibility with lablgtk | Maxime Dénès | |
| 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. | |||
| 2015-12-14 | Flag -compat 8.4 now loads Coq.Compat.Coq84. | Maxime Dénès | |
| 2015-12-14 | Moved proof_admitted to its own file, named "AdmitAxiom.v". | Maxime Dénès | |
| 2015-12-14 | Test file for #4363 was not complete. | Maxime Dénès | |
| 2015-12-14 | Extraction: cosmetically avoid generating spaces on empty lines | Pierre Letouzey | |
| 2015-12-14 | Remove some occurrences of Unix.opendir. | Guillaume Melquiond | |
| 2015-12-14 | Extraction: also get rid of explicit '\n' for haskell | Pierre Letouzey | |
| 2015-12-14 | Extraction: fix a pretty-print issue | Pierre Letouzey | |
| Some explicit '\n' in Pp.str were interacting badly with Format boxes in Compcert, leading to right-flushed "sig..end" blocks in some .mli | |||
| 2015-12-14 | Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty phrase") | Pierre Letouzey | |
| 2015-12-13 | More code sharing between tactic notation and genarg interpretation. | Pierre-Marie Pédrot | |
| 2015-12-12 | Extraction: documentation of the new option Unset Extraction SafeImplicits | Pierre Letouzey | |
| 2015-12-12 | Extraction: nicer implementation of Implicits | Pierre Letouzey | |
| 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. | |||
| 2015-12-12 | Extraction: check for remaining implicits after dead code removal (fix #4243) | Pierre Letouzey | |
| 2015-12-12 | Extraction: fix for bug #4334 (use of delta_resolver in Extract_env) | Pierre Letouzey | |
| 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. | |||
| 2015-12-12 | Extraction: avoid generating some blanks at end-of-line | Pierre Letouzey | |
| 2015-12-12 | Removing dead unsafe code in Genarg. | Pierre-Marie Pédrot | |
| 2015-12-12 | Indexing and documenting some options. | Pierre-Marie Pédrot | |
| 2015-12-11 | Optimize occur_evar_upto_types, avoiding repeateadly looking into the | Matthieu Sozeau | |
| same evar. | |||
| 2015-12-11 | Univs: Fix bug #4363, nested abstract. | Matthieu Sozeau | |
| 2015-12-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-11 | Document removal of Set Virtual Machine and -vm in CHANGES. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |