| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-09-13 | Merge PR #981: Miscellaneous fixes for notations | Maxime Dénès | |
| 2017-09-13 | Reference manual: A few words about the file system constraints for -Q/-R. | Hugo Herbelin | |
| 2017-09-13 | Adding a test for utf8 characters in directory names. | 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-13 | Supporting library names in utf8 in coqdep. | Hugo Herbelin | |
| 2017-09-13 | Fix GitLab CI | Gaëtan Gilbert | |
| - timing needs time and python - check for compiled files without source looks in the install directory (except for make -f Makefile.ci which doesn't check), as such the install directory has been renamed to _install_ci and isn't searched. | |||
| 2017-09-12 | Fixing bug #5693 (treating empty notation format as any format). | Hugo Herbelin | |
| A trick in counting spaces in a format was making the empty notation not behaving correctly. | |||
| 2017-09-12 | Adding a missing period in a notation warning. | Hugo Herbelin | |
| 2017-09-12 | Fixing bugs of a67bd7f9 and c6d9d4fb in recognizing a 'pat binding. | Hugo Herbelin | |
| Conditions for printing 'pat were incomplete. | |||
| 2017-09-12 | Don't exclude a priori CLocalDef to be treated by ppconstr.ml. | Hugo Herbelin | |
| 2017-09-12 | Fixing a typo in printing notations with recursive binders. | Hugo Herbelin | |
| Was causing a failure to print recursive binders used twice or more in the same notation. | |||
| 2017-09-12 | Fixing a bug of recursive notations introduced in dfdaf4de. | Hugo Herbelin | |
| When a proper notation variable occurred only in a recursive pattern of the notation, the notation was wrongly considered non printable due (the side effect that function compare_glob_constr and that mk_glob_constr_eq does not do anymore was indeed done by aux' but thrown away). This fixes it. | |||
| 2017-09-12 | Fixing little inaccuracy in coercions to ident or name. | Hugo Herbelin | |
| For instance, we don't want "id@{u}" to be coerced to id, or "?[n]" to "_". | |||
| 2017-09-12 | Adding function to be typically used to pass values from an OCaml "when" clause. | Hugo Herbelin | |
| 2017-09-12 | Removing now useless former fix to #3333 (check valid module names). | Hugo Herbelin | |
| The fix is not anymore needed after Id.of_string was made strict (5b218f87). This allows to support the whole official syntax of identifiers and not just the alpha-numerical ones (without quote). | |||
| 2017-09-12 | Port is_Set and is_Type to EConstr, as was is_Prop already. | Guillaume Melquiond | |
| 2017-09-11 | Better error messages, fix for BZ#5723 | Paul Steckler | |
| 2017-09-11 | Merge PR #1017: Addressing BZ#5713 (classical_left/classical_right ↵ | Maxime Dénès | |
| artificially restricted to a non-empty context). | |||
| 2017-09-11 | Remove unneeded fix for BZ#1715 | Gaëtan Gilbert | |
| It hasn't been necessary since 6aad0d9cd2104b5343ed7c831a4ad0bbe34007cb introduced $(INSTALLLIB) | |||
| 2017-09-11 | Merge PR #1032: Make our CI policy clearer and more explicit | Maxime Dénès | |
| 2017-09-11 | Disable OSX signing for temporary artifacts. | Maxime Dénès | |
| The OSX binaries were signed twice with a fake identity, leading to some obscure errors on Travis in some cases. We disable code signing for Travis artifacts. For released packages, a proper signing will be applied manually. | |||
| 2017-09-11 | Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit` | Maxime Dénès | |
| 2017-09-11 | Merge PR #1035: Fix the introduction of SSR refman chapter. | Maxime Dénès | |
| 2017-09-11 | Merge PR #1029: Fix a refine anomaly "Evar defined twice". | Maxime Dénès | |
| 2017-09-11 | Merge PR #1014: Add option index entry for NativeCompute Profiling | Maxime Dénès | |
| 2017-09-11 | Merge PR #1004: Document primitive projections in more detail | Maxime Dénès | |
| 2017-09-11 | Merge PR #987: In Array.smartmap, read and write from same array | Maxime Dénès | |
| 2017-09-11 | In stm, fixing a typo about flushing debugging messages. | Hugo Herbelin | |
| 2017-09-11 | Typo in the header of ide_slave.ml. | Hugo Herbelin | |
| 2017-09-11 | Coqide: adding a separating space in some debugging messages. | Hugo Herbelin | |
| This prevents seeing things like MsgDirectory which are actually intended to be two distinct words. | |||
| 2017-09-08 | Fix Typo in Doc for `Set Parsing Explicit` | staffehn | |
| 2017-09-08 | Normalizing universes before performing term comparison. | Pierre-Marie Pédrot | |
| This code was probably slightly wrong w.r.t. to a semantics defined as equivalent to first full-blown normalization followed by kernel term equality. Or at least, it was adding redundant constraints. | |||
| 2017-09-08 | Using EConstr equality check in unification. | Pierre-Marie Pédrot | |
| The code from Universes what essentially a duplicate of the one from EConstr, but they were copied for historical reasons. Now, this is not useful anymore, so that we remove the implementation from Universes and rely on the one from EConstr. | |||
| 2017-09-08 | Fix the introduction of SSR refman chapter. | Théo Zimmermann | |
| 2017-09-08 | Parse directly to Sorts.family when appropriate. | Gaëtan Gilbert | |
| When we used to parse to a glob_sort but always give an empty list in the GType case we can now parse directly to Sorts.family. | |||
| 2017-09-08 | Move README.ci and link to it from CONTRIBUTING. | Théo Zimmermann | |
| 2017-09-08 | Update CI policy. | Théo Zimmermann | |
| 2017-09-07 | Merge PR #997: coqdoc: Support comments in verbatim output | Maxime Dénès | |
| 2017-09-07 | Fix BZ#5655 by avoiding the creation of a cleaner thread for empty queues. | Maxime Dénès | |
| While this is a good workaround, Enrico has a minimal example of the underlying issue that we will send to the OCaml team. | |||
| 2017-09-07 | Merge PR #1016: 2 Typos in 'Add Parametric Morphism' Documentation | Maxime Dénès | |
| 2017-09-07 | Merge PR #968: Better error messages on the CI | Maxime Dénès | |
| 2017-09-07 | dev/build/windows/makecoq_mingw.sh: install camlp5's META file | Enrico Tassi | |
| 2017-09-07 | Merge PR #931: Parametrize module body | Maxime Dénès | |
| 2017-09-07 | Merge PR #914: Making the detyper lazy | Maxime Dénès | |
| 2017-09-07 | Merge PR #904: Add build_coq_or to API.Coqlib | Maxime Dénès | |
| 2017-09-07 | Trying to properly propagate errors in Windows CI script. | Maxime Dénès | |
| 2017-09-06 | use get_arguments, String.concat, remove -I | Paul Steckler | |
| 2017-09-06 | Fix a refine anomaly "Evar defined twice". | Pierre-Marie Pédrot | |
| Because the argument given to refine may mess with the evarmap, the goal being refined can be solved by side-effect after the term filler is computed. If this happens, we simply don't perform the refining operation. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |