| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-06-07 | Adding an only printing flag to notations. | Pierre-Marie Pédrot | |
| 2016-06-07 | Removing the use to Egramcoq.recover_constr_grammar. | Pierre-Marie Pédrot | |
| 2016-06-06 | Relying instead on the Coq85 inclusion! | Hugo Herbelin | |
| 2016-06-06 | Mode "Bracketing Last Introduction Pattern" is on for 8.4 | Hugo Herbelin | |
| and global for 8.4 and 8.5. | |||
| 2016-06-06 | Mode "Regular Subst Tactic" is on in 8.6. | Hugo Herbelin | |
| 2016-06-06 | Merge remote-tracking branch 'github/pr/118' into trunk | Maxime Dénès | |
| 2016-06-06 | About printing of traces of failures while calling ltac code. | Hugo Herbelin | |
| An Ltac trace printing mechanism was introduced in 8.4 which was inadvertedly modified by a series of commits such as 8e10368c3, 91f44f1da7a, ... It was also sometimes buggy, iirc, when entering ML tactics which themselves were calling ltac code. It got really bad in 8.5 as in: Tactic Notation "f" constr(x) := apply x. Ltac g x := f x. Goal False. idtac; f I. (* bad location reporting *) g I. (* was referring to tactic name "Top.Top#<>#1" *) which this commit fixes. I don't have a clear idea of what would be the best ltac tracing mechanism, but to avoid it to be broken without being noticed, I started to add some tests. Eventually, it might be worth that an Ltac expert brainstrom on it! | |||
| 2016-06-06 | xmlprotocol: fix unmarshaling of Feedback.Message | Enrico Tassi | |
| 2016-06-06 | xmlprotocol: uncomment marshalling code for custom message | Enrico Tassi | |
| 2016-06-06 | xmlprotocol: Marshal_error carries the reason | Enrico Tassi | |
| 2016-06-05 | Adding the Print Ltac Signatures command. | Pierre-Marie Pédrot | |
| 2016-06-05 | Adding the Print Ltac Signature command. | Pierre-Marie Pédrot | |
| 2016-06-05 | Remove Q_constr from grammar folder. | Pierre-Marie Pédrot | |
| 2016-06-05 | Removing the Q_constr file. | Pierre-Marie Pédrot | |
| 2016-06-05 | Moving Hipattern to a regular ML file. | Pierre-Marie Pédrot | |
| 2016-06-05 | Removing PATTERN uses in Hipattern. | Pierre-Marie Pédrot | |
| 2016-06-04 | Merge remote-tracking branch 'github/pr/184' into trunk | Maxime Dénès | |
| 2016-06-03 | Remove a few tactics from the Tacexpr AST. | Pierre-Marie Pédrot | |
| Note that this breaks a few badly written scripts using intro in strict mode without providing an existing identifier. | |||
| 2016-06-03 | Removing "rename" from the tactic AST. | Pierre-Marie Pédrot | |
| 2016-06-03 | Removing "exact" from the tactic AST. | Pierre-Marie Pédrot | |
| 2016-06-03 | Removing "intro" from the tactic AST. | Pierre-Marie Pédrot | |
| Note that this breaks the compatibility, in a beneficial way I believe. Tactics defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction on a local identifier anymore. They must use the "fresh" primitive instead. | |||
| 2016-06-03 | Removing "double induction" from the tactic AST. | Pierre-Marie Pédrot | |
| 2016-06-03 | Merge remote-tracking branch 'github/pr/159' into trunk | Maxime Dénès | |
| 2016-06-03 | Fix build of documentation (broken for four months). | Guillaume Melquiond | |
| 2016-06-03 | Merge branch 'v8.5' into trunk | Guillaume Melquiond | |
| 2016-06-03 | Fix proof terminators not being detected in presence of curly brackets (bug ↵ | Guillaume Melquiond | |
| #4770). This also fixes comments not being properly skipped when looking for eol. | |||
| 2016-06-03 | Make "coqdoc -g --parse-comments" behave properly (bug #4773). | Guillaume Melquiond | |
| As a side effect, there should be a small speedup when ignoring comments. This commit also fixes two bugs related to handling "$$" and "#" in comments. | |||
| 2016-06-02 | Please never mention .mli-only file in *.mllib (or future *.mlpack) | Pierre Letouzey | |
| This breaks compilation via ocamlbuild, and also leads to awkward commands via make | |||
| 2016-06-02 | Add documentation to the low-level `Pp` functions. | Emilio Jesus Gallego Arias | |
| Thanks to HH for pointing it out. | |||
| 2016-06-02 | Move XML serialization to ide/ folder. | Pierre-Marie Pédrot | |
| 2016-06-02 | Move ide serialization libraries from lib/ to ide/ | Emilio Jesus Gallego Arias | |
| This makes the core free from particular protocol choices. It should help with the ppx serialization project and shrinks clib.cma a bit. | |||
| 2016-06-02 | Encapsulate xml serialization in xmlprotocol.mli | Emilio Jesus Gallego Arias | |
| This eases the task of replacing/improving the serializer, as well as making it more resistant. See pitfalls below: Main changes are: - fold `message` type into `feedback` type - make messages of type `Richpp.richpp` so we are explicit about the content being a rich document. - moved serialization functions for messages and stateid to `Xmlprotocol` - improved a couple of internal API points (`is_message`). Tested. | |||
| 2016-06-02 | Move serialization functions out of Stm | Emilio Jesus Gallego Arias | |
| Serialization should be specific to each particular backend, so we let the Stm clients choose how the send the nodes. This should be quite safe to pull in. Test suite passes. Related to #180 | |||
| 2016-06-02 | Fix build (use the same mllib file as in trunk). | Guillaume Melquiond | |
| 2016-06-02 | Avoid refreshing the segment widget each time a sentence is added. | Lionel Rieg | |
| This brings a 10x speedup for going at the end of large .v files. | |||
| 2016-06-02 | Fix bug #4768. | Guillaume Melquiond | |
| 2016-06-02 | Makefile.build: clean a bit the way MacOS binaries are signed | Pierre Letouzey | |
| 2016-06-02 | Avoid refreshing the segment widget each time a sentence is added. | Lionel Rieg | |
| This brings a 10x speedup for going at the end of large .v files. | |||
| 2016-06-02 | A slight phase of documentation and uniformization of names of | Hugo Herbelin | |
| functions about interpretation, internalization, externalization of notations. Main syntactic changes: - subst_aconstr_in_glob_constr -> instantiate_notation_constr (because aconstr has been renamed to notation_constr long time ago) - extern_symbol -> extern_notation (because symbol.ml has been renamed to notation.ml long time ago) - documentation of notations_ops.mli Main semantic changes: - Notation_ops.eq_glob_constr which was partial eq disappears: use glob_constr_eq instead - In particular, this impacts a change on funind which now use the (fully implemented) glob_constr_eq Somehow, instantiate_notation_constr should be in notation_ops.ml for symmetry with match_notation_constr but it is bit painful to do. | |||
| 2016-06-02 | Makefile.common: update PRIVATEBINARIES to repair the build on MACOS | Pierre Letouzey | |
| 2016-06-02 | coqtop: Add ltac/ to search path. | Matthieu Sozeau | |
| For Drop for example. | |||
| 2016-06-02 | Removing pointless field NPatVar. It does not make sense to have Meta | Hugo Herbelin | |
| and Evar in notations, and there are anyway already forbidden. | |||
| 2016-06-02 | Update primitive coinductive test-suite. | Matthieu Sozeau | |
| 2016-06-02 | Add a synonymous Set Debug Ltac for Set Ltac Debug, for uniformity. | Hugo Herbelin | |
| 2016-06-02 | Add a synonymous Set Debug Typeclasses for Set Typeclasses Debug, for ↵ | Hugo Herbelin | |
| uniformity. | |||
| 2016-06-01 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-06-01 | Makefile.build : follow-up of previous commit | Pierre Letouzey | |
| - the particlar rule for dev/printers.cma is adapted as for %.cma:%.mllib - some more removal of | .d in rules | |||
| 2016-06-01 | Makefile.build : improved rules about .cm(x)a | Pierre Letouzey | |
| We add a dependency of .cma over .mllib. This dependency over the .mllib is somewhat artificial, since ocamlc -a won't use this file, hence the $(filter-out ...) below. But this ensures that the .cm(x)a is rebuilt when needed, (especially when removing a module in the .mllib). We also remove all "order-only" dependencies over *.d in rules, since the -include mechanism should already ensure that we have up-to-date dependencies known by make. | |||
| 2016-06-01 | Makefile.build : update the otags rule | Pierre Letouzey | |
| There were a forgotten CAMLP4DEPS macro. We also avoid otags failure with camlp5 (in this case, it only builds the tags of regular .ml files, not .ml4). | |||
| 2016-06-01 | g_tactics : remove opt_bindings (2-line dead code) | Pierre Letouzey | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |