| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-09-15 | Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵ | Maxime Dénès | |
| top of the linking chain. | |||
| 2017-09-15 | Merge PR #1051: Using an algebraic type for distinguishing toplevel input ↵ | Maxime Dénès | |
| from location in file | |||
| 2017-09-15 | Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already. | Maxime Dénès | |
| 2017-09-15 | Merge PR #1046: Better error messages, fix for BZ#5723 | Maxime Dénès | |
| 2017-09-15 | Merge PR #1045: Remove unneeded fix for BZ#1715 | Maxime Dénès | |
| 2017-09-15 | Merge PR #1042: Fixing minor typos in stm/coqide | Maxime Dénès | |
| 2017-09-15 | Merge PR #1000: Update CREDITS on a best-effort basis. | Maxime Dénès | |
| 2017-09-15 | Merge PR #1037: Parse directly to Sorts.family when appropriate. | Maxime Dénès | |
| 2017-09-15 | Merge PR #1025: BZ#5716, read flags from project file for Compile Buffer | Maxime Dénès | |
| 2017-09-15 | Add debug output to brew update. | Maxime Dénès | |
| 2017-09-15 | Switch Travis to OSX 10.12 and Xcode 8.3.3. | Maxime Dénès | |
| 2017-09-15 | Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" ↵ | Maxime Dénès | |
| Inductive-keyworded record failing even on non-dependent goal) | |||
| 2017-09-15 | Merge PR #990: Prevent warning about DSTROOT being undefined. | Maxime Dénès | |
| 2017-09-15 | Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" ↵ | Maxime Dénès | |
| work better on them | |||
| 2017-09-15 | Merge PR #962: Move dev/doc/changes to Markdown. | Maxime Dénès | |
| 2017-09-15 | Merge PR #955: Do not hashcons universes beforehand | Maxime Dénès | |
| 2017-09-15 | Merge PR #938: [parsing] Remove hacks for reduced Prelude. | Maxime Dénès | |
| 2017-09-15 | Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match ↵ | Maxime Dénès | |
| anonymous variables) | |||
| 2017-09-15 | Phantom type for typed closures. | Pierre-Marie Pédrot | |
| 2017-09-14 | Abstracting away the type of arities and ML tactics. | Pierre-Marie Pédrot | |
| 2017-09-14 | Moving valexpr definition to Tac2ffi. | Pierre-Marie Pédrot | |
| 2017-09-14 | Explicit arity for closures. | Pierre-Marie Pédrot | |
| 2017-09-14 | Introducing the remember tactic. | Pierre-Marie Pédrot | |
| 2017-09-14 | Using an algebraic type for distinguishing toplevel input from location in file. | Hugo Herbelin | |
| 2017-09-14 | Avoid extra failure in the "constructor" tactic (bug #5666). | Guillaume Melquiond | |
| This changes the implementation of "constructor" from constructor 1 + ... + constructor n + fail to constructor 1 + ... + constructor n. | |||
| 2017-09-14 | Binding the pose/set family of tactics. | Pierre-Marie Pédrot | |
| 2017-09-14 | Use a simpler syntax for generalize grammar. | Pierre-Marie Pédrot | |
| This removes the use for a quotation. | |||
| 2017-09-13 | Better printing for list literals. | Pierre-Marie Pédrot | |
| 2017-09-13 | Adding quotations for the generalize tactic. | Pierre-Marie Pédrot | |
| 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) | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |