| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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) | |||
| 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-09 | If backtrace is missing, don't print it. | Pierre-Marie Pédrot | |
| 2017-09-09 | Update backtraces only when the Ltac2 Backtrace flag is set. | Pierre-Marie Pédrot | |
| 2017-09-09 | Fix coq/ltac2#26: Ltac1 gives no backtraces. | Pierre-Marie Pédrot | |
| 2017-09-09 | Fix coq/ltac2#18: Terms should show a backtrace when Set Ltac2 Backtrace is set. | Pierre-Marie Pédrot | |
| 2017-09-09 | Moving Ltac2 backtraces to the Exninfo mechanism. | Pierre-Marie Pédrot | |
| I don't know why, but on CoqIDE this triggers a printing of the backtrace twice. This is not reproducible with coqtop. | |||
| 2017-09-09 | Fix coq/ltac2#25: Control.case should not be able to catch Control.throw. | Pierre-Marie Pédrot | |
| When crossing constr boundaries, we mark exceptions as being fatal not to catch them. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |