| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-09-11 | Merge PR #987: In Array.smartmap, read and write from same array | Maxime Dénès | |
| 2017-09-04 | Making detyping potentially lazy. | Pierre-Marie Pédrot | |
| The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager. | |||
| 2017-08-31 | Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name | Maxime Dénès | |
| 2017-08-31 | Merge PR #989: Prevent overallocation in Array.map_to_list and remove custom ↵ | Maxime Dénès | |
| implementation from Detyping. | |||
| 2017-08-29 | Merge PR #773: [flags] Remove XML output flag. | Maxime Dénès | |
| 2017-08-29 | Canonically renaming fold_map into fold_left_map in library Option. | Hugo Herbelin | |
| Also adding fold_right_map by consistency. | |||
| 2017-08-29 | Canonically renaming fold_map into fold_left_map in library Array. | Hugo Herbelin | |
| Also renaming fold_map' into fold_right_map, and fold_map2' into fold_right2_map. | |||
| 2017-08-29 | Adding combinators + a canonical renaming in cList.ml. | Hugo Herbelin | |
| - Adding fold_left2_map/fold_right2_map. - Canonically renaming fold_map/fold_map' into fold_left_map/fold_right_map. | |||
| 2017-08-22 | also in Fun1.smartmap, read, write from same array | Paul Steckler | |
| 2017-08-22 | Prevent overallocation in Array.map_to_list and remove custom implementation ↵ | Guillaume Melquiond | |
| from Detyping. | |||
| 2017-08-21 | read, write from same array | Paul Steckler | |
| 2017-08-17 | Merge PR #490: A possible fix for #5391 (command line tools do not accept ↵ | Maxime Dénès | |
| trailing / and \ on windows) | |||
| 2017-08-16 | Merge PR #864: Some cleanups after cumulativity for inductive types | Maxime Dénès | |
| 2017-08-15 | Removing trailing "/" and "\" in directory names only on win32. | Hugo Herbelin | |
| This refines e234f3ef. By the way, note that e234f3ef fixed #5391 (command line tools do not accept trailing "/" - or "\" - in windows). | |||
| 2017-08-01 | [flags] Remove XML output flag. | Emilio Jesus Gallego Arias | |
| This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied. | |||
| 2017-07-31 | Change the option for cumulativity | Amin Timany | |
| 2017-07-31 | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | Maxime Dénès | |
| 2017-07-27 | deprecate Pp.std_ppcmds type alias | Matej Košík | |
| 2017-07-26 | Merge PR #902: Only perform profile initialization and printing when the ↵ | Maxime Dénès | |
| flag is set. | |||
| 2017-07-21 | Adding a V8.7 compatibility version number. | Hugo Herbelin | |
| 2017-07-21 | PMP sold us a Timeout on Windows with 1s resolution. Trying to improve it. | Maxime Dénès | |
| 2017-07-20 | coq_makefile: use System.exists_dir for better portability | Enrico Tassi | |
| 2017-07-20 | Windows: Sys.is_dir "foo/" always says no (so we strip trailing slash) | Enrico Tassi | |
| 2017-07-20 | Also a less intrusive Profile.init_profile. | Hugo Herbelin | |
| Calling it only when there is something to profile, or when profiling is explicitly required with the profile flags, so that profiling in plugins is possible. | |||
| 2017-07-20 | A less intrusive Profile.close_profile. | Hugo Herbelin | |
| No need to call Gc functions nor Unix timing functions when there is nothing to report. Moreover, PMP observed problems with these functions in the debugger. PMP also reported that Gc.minor takes some noticeable time, so no need to trigger some when unneeded. | |||
| 2017-07-20 | Merge PR #898: [pp] Fix bugs 5651 [incorrect thunk in pretty printer] | Maxime Dénès | |
| 2017-07-20 | Merge PR #869: Enforce alternating separators in typeclass debug output | Maxime Dénès | |
| 2017-07-19 | [pp] Fix bugs 5651 [incorrect thunk in pretty printer] | Emilio Jesus Gallego Arias | |
| Fix bug introduced by a Haskell programmer. | |||
| 2017-07-17 | Merge PR #862: Adding support for bindings tags to explicit prefix/suffix ↵ | Maxime Dénès | |
| rather than colors | |||
| 2017-07-12 | format pairs of items for pr_depth to get alternating separators | Paul Steckler | |
| eval thunks once in prlist_sep_lastsep, make code clearer add typeclass debug output test | |||
| 2017-07-08 | Adding support for bindings tags to explicit prefix/suffix rather than colors. | Hugo Herbelin | |
| This is usable for no-color terminal. For instance, a typical application in mind is the Coq-generate names marker which can be rendered with a color if the interface supports it and a prefix "~" if the interface does not support colors. | |||
| 2017-07-05 | use Int.equal instead of polymorphic = | Paul Steckler | |
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2017-06-23 | Fix bug 5392: Warnings defined in plugins are considered unknown | Maxime Dénès | |
| The status of a warning can now be set before the warning is declared (typically by a plugin). However, I had to remove the "unknown warning" warning. | |||
| 2017-06-19 | Merge PR#613: Cumulativity for inductive types | Maxime Dénès | |
| 2017-06-19 | Fix typo in comment. | Maxime Dénès | |
| 2017-06-16 | Fix bugs and add an option for cumulativity | Amin Timany | |
| 2017-06-15 | Merge PR#375: Deprecation | Maxime Dénès | |
| 2017-06-14 | Merge PR#739: completing a sentence in a comment | Maxime Dénès | |
| 2017-06-14 | Remove support for Coq 8.4. | Guillaume Melquiond | |
| 2017-06-14 | Remove support for Coq 8.3. | Guillaume Melquiond | |
| 2017-06-14 | Remove support for Coq 8.2. | Guillaume Melquiond | |
| 2017-06-14 | Add a version to be used when parsing compatibility notations mentioning old ↵ | Guillaume Melquiond | |
| versions. | |||
| 2017-06-12 | Add support for "-bypass-API" argument of "coq_makefile" | Matej Košík | |
| Plugin-writers can now use: -bypass-API parameter with "coq_makefile". The effect of that is that instead of -I API the plugin will be compiled with: -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac | |||
| 2017-06-07 | completing a sentence in a comment | Matej Košík | |
| 2017-06-07 | Put all plugins behind an "API". | Matej Kosik | |
| 2017-06-06 | Merge PR#728: A few typos. | Maxime Dénès | |
| 2017-06-04 | A few typos. | Hugo Herbelin | |
| 2017-06-02 | Drop '.' from CErrors.anomaly, insert it in args | Jason Gross | |
| As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ``` | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |