| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-01-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-01-22 | Restore warnings produced by the interpretation of the command line | Hugo Herbelin | |
| (e.g. with deprecated options such as -byte, etc.) since I guess this is what we expect. Was probably lost in 81eb133d64ac81cb. | |||
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-01-21 | Stronger invariants on the use of the introduction pattern (pat1,...,patn). | Hugo Herbelin | |
| The length of the pattern should now be exactly the number of assumptions and definitions introduced by the destruction or induction, including the induction hypotheses in case of an induction. Like for pattern-matching, the local definitions in the argument of the constructor can be skipped in which case a name is automatically created for these. | |||
| 2016-01-20 | Update copyright headers. | Maxime Dénès | |
| 2016-01-17 | Moving val_cast to Tacinterp. | Pierre-Marie Pédrot | |
| 2016-01-17 | Getting rid of the awkward unpack mechanism from Genarg. | Pierre-Marie Pédrot | |
| 2016-01-17 | Simplification and type-safety of Pcoq thanks to GADTs in Genarg. | Pierre-Marie Pédrot | |
| 2016-01-17 | Exporting Genarg implementation in the API. | Pierre-Marie Pédrot | |
| We can now use the expressivity of GADT to work around historical kludges of generic arguments. | |||
| 2016-01-17 | Reimplementing Genarg safely. | Pierre-Marie Pédrot | |
| No more Obj.magic in Genarg. We leverage the expressivity of GADT coupled with dynamic tags to get rid of unsafety. For now the API did not change in order to port the legacy code more easily. | |||
| 2016-01-17 | Adding a structure indexed by tags. | Pierre-Marie Pédrot | |
| 2016-01-17 | Temporary commit getting rid of Obj.magic unsafety for Genarg. | Pierre-Marie Pédrot | |
| This will allow an easier landing of the rewriting of Genarg. | |||
| 2016-01-15 | Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen. | Maxime Dénès | |
| 2016-01-14 | Removing constr generic argument. | Pierre-Marie Pédrot | |
| 2016-01-14 | Removing ident and var generic arguments. | Pierre-Marie Pédrot | |
| 2016-01-06 | Merge remote-tracking branch 'origin/v8.5' into trunk | Guillaume Melquiond | |
| Conflicts: lib/cSig.mli | |||
| 2016-01-06 | Protect code against changes in Map interface. | Maxime Dénès | |
| The Map interface of upcoming OCaml 4.03 includes a new union operator. In order to make our homemade implementation of Maps compatible with OCaml versions from 3.12 to 4.03, we define our own signatures for Maps. | |||
| 2016-01-05 | Fix order of files in mllib. | Maxime Dénès | |
| CString was linked after Serialize, although the later was using CString.equal. This had not been noticed so far because OCaml was ignoring functions marked as external in interfaces (which is the case of CString.equal) when considering link dependencies. This was changed on the OCaml side as part of the fix of PR#6956, so linking was now failing in several places. | |||
| 2016-01-05 | COMMENTS: Predicate | Matej Kosik | |
| In the original version, ocamldoc markup wasn't used properly thus ocamldoc output did not in all places make sense. This commit makes sure that the documentation of the Predicate module is as clear as the documentation of the Set module (in the standard library). | |||
| 2016-01-02 | Remove some unused functions. | Guillaume Melquiond | |
| Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. | |||
| 2016-01-02 | Remove some useless module opening. | Guillaume Melquiond | |
| 2016-01-02 | Avoid warnings about loop indices. | Guillaume Melquiond | |
| 2016-01-01 | Fix typos. | Guillaume Melquiond | |
| 2016-01-01 | Remove unused hashconsing code. | Guillaume Melquiond | |
| 2016-01-01 | Do not make it harder on the compiler optimizer by packing arguments. | Guillaume Melquiond | |
| 2015-12-31 | Merge branch 'v8.5' into trunk | Guillaume Melquiond | |
| 2015-12-31 | Do not compose List.length with List.filter. | Guillaume Melquiond | |
| 2015-12-31 | Do not dump a glob reference when its location is ghost. (Fix bug #4469) | Guillaume Melquiond | |
| This patch also causes the code to finish a bit faster in the NoGlob case by not preparing a string for dump_string. It also optimizes Dumpglob.is_ghost by only checking whether the end position is zero. Note that no ghost locations were part of the glob files of the standard library before the patch. Note also that the html documentation of the standard library is bitwise identical before and after the patch. | |||
| 2015-12-28 | Removing the special status of open_constr generic argument. | Pierre-Marie Pédrot | |
| We also intepret it at toplevel as a true constr and push the resulting evarmap in the current state. | |||
| 2015-12-21 | Finer-grained types for toplevel values. | Pierre-Marie Pédrot | |
| 2015-12-21 | Removing ad-hoc interpretation rules for tactic notations and their genarg. | Pierre-Marie Pédrot | |
| Now that types can share the same dynamic representation, we do not have to transtype the topelvel values dynamically and just take advantage of the standard interpretation function. | |||
| 2015-12-21 | Sharing toplevel representation for several generic types. | Pierre-Marie Pédrot | |
| - int and int_or_var - ident and var - constr and constr_may_eval | |||
| 2015-12-21 | Removing the now useless genarg generic argument. | Pierre-Marie Pédrot | |
| 2015-12-21 | Using dynamic values in tactic evaluation. | Pierre-Marie Pédrot | |
| 2015-12-21 | Attaching a dynamic argument to the toplevel type of generic arguments. | Pierre-Marie Pédrot | |
| 2015-12-21 | Trust the directory cache in batch mode. | Guillaume Melquiond | |
| When coqtop is a long-lived process (e.g. coqide), the user might be creating files on the fly. So we have to ask the operating system whether a file exists beforehand, so that we know whether the content of the directory cache is outdated. In batch mode, we can assume that the cache is always up-to-date, so we don't need to query the operating system before trusting the content of the cache. On a script doing "Require Import Reals", this brings down the number of stat syscalls from 42k to 2k. The number of syscalls could be further halved if all_subdirs was filling the directory cache. | |||
| 2015-12-18 | COMMENTS: added to the "Unicode" module. | Matej Kosik | |
| 2015-12-18 | COMMENTS: updated in the "Option" module. | Matej Kosik | |
| 2015-12-18 | COMMENTS: added to the "Predicate" module | Matej Kosik | |
| In the original version, ocamldoc markup wasn't used properly thus ocamldoc output did not in all places make sense. This commit makes sure that the documentation of the Predicate module is as clear as the documentation of the Set module (in the standard library). | |||
| 2015-12-17 | spawn: fix leak of file descriptors | Enrico Tassi | |
| The interesting manifestation of the bug was Unix.select returning no error but the empty list of descriptors, as if a timeout did happen. | |||
| 2015-12-17 | Getting rid of some hardwired generic arguments. | Pierre-Marie Pédrot | |
| 2015-12-14 | Adding compatibility flag for 8.5. | Hugo Herbelin | |
| Soon needing a more algebraic view at version numbers... | |||
| 2015-12-14 | Remove some occurrences of Unix.opendir. | Guillaume Melquiond | |
| 2015-12-12 | Removing dead unsafe code in Genarg. | Pierre-Marie Pédrot | |
| 2015-12-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-10 | Fixing compilation with OCaml 3.12 after commit 9d45d45f3a87 on removing | Hugo Herbelin | |
| "open Unix" from lib/system.ml. | |||
| 2015-12-09 | Remove remaining occurrences of Unix.readdir. | Guillaume Melquiond | |
| 2015-12-09 | Replace Unix.readdir by Sys.readdir in dir cache. | Emilio Jesus Gallego Arias | |
| This makes the function sightly more portable. | |||
| 2015-12-05 | Factorizing unsafe code by relying on the new Dyn module. | Pierre-Marie Pédrot | |
| 2015-12-05 | Leveraging GADTs to provide a better Dyn API. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |