| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-03-18 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-03-17 | Removing the registering of default values for generic arguments. | Pierre-Marie Pédrot | |
| 2016-03-17 | Reducing the number of modules linked in grammar.cma. | Pierre-Marie Pédrot | |
| 2016-03-15 | Fix #4591: Uncaught exception in directory browsing. | Pierre-Marie Pédrot | |
| We protect Sys.readdir calls againts any nasty exception. | |||
| 2016-03-13 | Adding a few functions on type union. | Hugo Herbelin | |
| 2016-03-10 | Removing OCaml deprecated function names from the Lazy module. | Pierre-Marie Pédrot | |
| 2016-03-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-03-09 | Win: kill unreliable hence do not waitpid after kill -9 (Close #4369) | Enrico Tassi | |
| This commit also completes 74bd95d10b9f4cccb4bd5b855786c444492b201b | |||
| 2016-03-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-03-04 | Rename Ephemeron -> CEphemeron. | Maxime Dénès | |
| Fixes compilation of Coq with OCaml 4.03 beta 1. | |||
| 2016-03-03 | Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop. | Pierre-Marie Pédrot | |
| Printing invalid UTF-8 string startled GTK too much, leading to CoqIDE dying improperly. We now check that all strings outputed by Coq are proper UTF-8. This is not perfect, as CoqIDE will sometimes truncate strings which contains the null character, but at least it should not crash. | |||
| 2016-02-17 | CLEANUP: Renaming "Util.compose" function to "%" | Matej Kosik | |
| I propose to change the name of the "Util.compose" function to "%". Reasons: 1. If one wants to express function composition, then the new name enables us to achieve this goal easier. 2. In "Batteries Included" they had made the same choice. | |||
| 2016-02-13 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-02-10 | Don't fail fatally if PATH is not set. | Emilio Jesus Gallego Arias | |
| This fixes micromega in certain environments. | |||
| 2016-02-03 | Adding a "get" primitive to map signature. | Pierre-Marie Pédrot | |
| It is similar to find but raises an assertion failure instead of a Not_found when the element is not encountered. Using it will give stronger invariants. | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |