| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2015-12-11 | Remove Set Virtual Machine from doc, since the command itself has been removed. | Maxime Dénès | |
| 2015-12-11 | Add tactic native_cast_no_check, analog to vm_cast_no_check. | Maxime Dénès | |
| 2015-12-10 | Fixing a pat%constr bug. Thanks to Enrico for reporting. | Hugo Herbelin | |
| 2015-12-10 | Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn. | Hugo Herbelin | |
| Marking it as experimental. | |||
| 2015-12-10 | Fixing compilation with OCaml 3.12 after commit 9d45d45f3a87 on removing | Hugo Herbelin | |
| "open Unix" from lib/system.ml. | |||
| 2015-12-10 | Silently ignore requests to _not_ clear something when that something cannot ↵ | Guillaume Melquiond | |
| be cleared. This should fix the contrib failures on tactics like "destruct (0)". | |||
| 2015-12-10 | Refman, ch. 4: A few fixes. | Hugo Herbelin | |
| 2015-12-10 | ENH: redundant examples were removed | Matej Kosik | |
| 2015-12-10 | FIX: wrong reference to a figure | Matej Kosik | |
| 2015-12-10 | CLEANUP: putting examples inside "figure" environment | Matej Kosik | |
| 2015-12-10 | ENH: The definition of the "_ ; _" operation on local context was added. | Matej Kosik | |
| 2015-12-10 | TYPOGRAPHY: adjustments | Matej Kosik | |
| 2015-12-10 | PROPOSITION: the side-condition was made more specific. | Matej Kosik | |
| 2015-12-10 | PROPOSITION: rephrasing of the explanation of the meaning of '[I:A|B]' | Matej Kosik | |
| 2015-12-10 | PROPOSITION: Added an explicit definition of the notation for enriching the ↵ | Matej Kosik | |
| global environment (we use throughout the document) | |||
| 2015-12-10 | PROPOSITION: Added "if" and "then" words missing in the original sentence. | Matej Kosik | |
| 2015-12-10 | PROPOSITION: Example was simplified | Matej Kosik | |
| 2015-12-10 | DONE | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | TYPOGRAPHY | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |