| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-10-03 | Merge PR #1100: Avoid looping when searching for CoqProject. | Maxime Dénès | |
| 2017-10-03 | Merge PR #1015: Adding a function to be typically used to pass values from ↵ | Maxime Dénès | |
| an OCaml "when" clause to the r.h.s of the matching clause | |||
| 2017-09-27 | Avoid looping when searching for CoqProject. | Maxime Dénès | |
| This could happen with paths on Windows, or even relative paths on all OSs. Fixes #5730: CoqIDE becomes unresponsive on file open. | |||
| 2017-09-21 | Improve support for "-w none" compatibility option. | Guillaume Melquiond | |
| If coqtop was started with "-w none" yet the script used "Set Warnings Append", then all the warnings were turned back to their default value. This commit turns "none" (whatever its sign) into "-all" whenever some warning status is modified afterward, in order to prevent the issue. | |||
| 2017-09-19 | coq_makefile: make sure compile flags for Coq and coq_makefile are in sync | Emilio Jesus Gallego Arias | |
| E.g. -safe-string is set by configure.ml and made available to both make (via config/Makefile) and coq_makefile (via config/coq_config.ml -> lib/envars.ml -> CoqMakefile.in). | |||
| 2017-09-18 | Reporting locations in error messages about notation formats. | Hugo Herbelin | |
| 2017-09-14 | Using an algebraic type for distinguishing toplevel input from location in file. | Hugo Herbelin | |
| 2017-09-13 | A possible fix for BZ#5715 (escape non-utf8 win32 file names). | Hugo Herbelin | |
| On Win32, Sys.readdir translates the file names to the charset of the local "code page", which may be not compatible with utf8. Warnings referring to these names can be generated. These warnings may be sent to CoqIDE. To ensure a utf8 compliant communication, we escape non-utf8 file names under win32. In the CoqIDE/Coq communication, Glib.IO.read_chars expects an utf8-encoding and raises otherwise a Glib.Error "Invalid byte sequence in conversion input". This fixes bug #5715 (Hangul characters not recognized in file names) but this does not solve the case of an operating system mounting a file system with a different coding convention than the default one, i.e. unicode using "Normalization Form Canonical Decomposition" in UTF-8 for HFS+ on MacOS X, no encoding for ext3/ext4 on Linux, (non-normalized?) UTF-16 for NTFS on Windows. | |||
| 2017-09-13 | Complying more precisely to unicode standard. | Hugo Herbelin | |
| In particular, checking that it is at most 4 bytes. | |||
| 2017-09-13 | Adding a function to escape strings with non-utf8 characters. | Hugo Herbelin | |
| 2017-09-12 | Adding function to be typically used to pass values from an OCaml "when" clause. | Hugo Herbelin | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |