| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-05-04 | typo | Enrico Tassi | |
| 2016-05-04 | Moving the Val module to Geninterp. | Pierre-Marie Pédrot | |
| 2016-05-04 | Switching to an untyped toplevel representation for Ltac values. | Pierre-Marie Pédrot | |
| 2016-05-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-04-25 | Print magic numbers in bad magic error message | Tej Chajed | |
| 2016-04-20 | Adding an OCaml printer for pre-initialization anomalies. | Pierre-Marie Pédrot | |
| 2016-04-15 | Cleaning unpolished commit 0dfd0fb7d7 on basic functions about union type. | Hugo Herbelin | |
| 2016-04-09 | In pr_clauses, do not print a leading space by default so that it can | Hugo Herbelin | |
| be used in the generic printer for tactics. Allows e.g. to print "symmetry in H" correctly after its move to TACTIC EXTEND. | |||
| 2016-04-08 | Fixing printing of toplevel values. | Pierre-Marie Pédrot | |
| This is not perfect yet, in particular the whole precedence system is a real mess, as there is a real need for tidying up the Pptactic implementation. Nonetheless, printing toplevel values is only used for debugging purposes, where an ugly display is better than none at all. | |||
| 2016-03-30 | Ensuring that the type of base generic arguments contain triples. | Pierre-Marie Pédrot | |
| 2016-03-30 | Removing dead code in Genarg. | Pierre-Marie Pédrot | |
| 2016-03-30 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-03-22 | A patch renaming equal into eq in the module dealing with | Hugo Herbelin | |
| hash-consing, so as to avoid having too many kinds of equalities with same name. | |||
| 2016-03-19 | Removing dead code in Genarg. | Pierre-Marie Pédrot | |
| 2016-03-19 | Removing the untyped representation of genargs. | Pierre-Marie Pédrot | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |