| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-07-21 | Fix bug #4679, weakened setoid_rewrite unification | Matthieu Sozeau | |
| It should use evar instantiations eagerly during unification of the lhs of the lemma, as in 8.4. | |||
| 2016-07-20 | Update CHANGES | Matthieu Sozeau | |
| 2016-07-20 | Fix bug #4780: universe leak in letin_tac | Matthieu Sozeau | |
| 2016-07-19 | Complementing previous commit on fixes for printing binding patterns. | Hugo Herbelin | |
| 2016-07-19 | Some extra fixes in printing patterns in binders. | Hugo Herbelin | |
| - typo in notation_ops.ml - factorization of patterns in ppconstr.ml - update of test-suite - printing of cast of a binding pattern if in mode "printing all" The question of whether or not to print the type of a binding pattern by default seems open to me. | |||
| 2016-07-19 | Taking into account binding patterns when agglutinating sequences of binders. | Hugo Herbelin | |
| Supporting accordingly printing of sequences of binders including binding patterns. | |||
| 2016-07-19 | Notations with multiple recursive binders: fixing use of alpha-conversion. | Hugo Herbelin | |
| 2016-07-19 | Fixing missing parentheses in printing of patterns in binders. | Hugo Herbelin | |
| (In agreement with Daniel.) | |||
| 2016-07-19 | Notations: fixing multiple binders used as terms in reverse order. | Hugo Herbelin | |
| 2016-07-19 | Removing a source of clash with multiple recursive patterns in notations. | Hugo Herbelin | |
| The same variable name was used to collect the binders and the successive steps of matching one binder, resulting in unexpected attempts for merging in the presence of multiple occurrence of the same recursive pattern. An amusing side-effect: when eta-expanding for a notation with recursive binders, it is the second variable of the "x .. y" which is used to invent a name rather than the first one. | |||
| 2016-07-19 | Fixing extra returns in top_printers.ml (msg_notice not same semantics as pp). | Hugo Herbelin | |
| 2016-07-18 | A new step on using alpha-conversion in printing notations. | Hugo Herbelin | |
| A couple of bugs have been found. Example #4932 is now printing correctly in the presence of multiple binders (when no let-in, no irrefutable patterns). | |||
| 2016-07-18 | Replacing deprecated Implicit Arguments in prelude. | Maxime Dénès | |
| Was triggering a deprecation warning. | |||
| 2016-07-18 | Remove the swap tactic from the prelude. | Maxime Dénès | |
| It was anyway unusable due to a parsing conflict with the swap operator on goals. Was triggering a warning when compiling the prelude. | |||
| 2016-07-18 | Marking bug #3383 as solved. | Pierre-Marie Pédrot | |
| 2016-07-18 | Fix bug #4923: Warning: appcontext is deprecated. | Pierre-Marie Pédrot | |
| 2016-07-18 | Removing useless grammar entries. Fixes bug #4919. | Pierre-Marie Pédrot | |
| 2016-07-17 | Partial fix to #4592 (notation requiring alpha-conversion for printing). | Hugo Herbelin | |
| 2016-07-17 | More examples of recursive notations, with emphasis in reference manual. | Hugo Herbelin | |
| Further work would include: - Identify binders up to alpha-conversion (see #4932 with a list of binders of length at least 2, or #4592 on printing notations such as ex2). A cool example that one could also consider supporting: - Notation "[[ a , .. , b | .. | a , .. , b ]]" := (cons (cons a .. (cons b nil) ..) .. (cons a .. (cons b nil) ..) ..). | |||
| 2016-07-17 | Fixing a bug in recognizing a recursive pattern of notations | Hugo Herbelin | |
| immediately in the scope of another recursive pattern. | |||
| 2016-07-17 | Fixing interpretation of notations w/ opposite instances of a recursive pattern. | Hugo Herbelin | |
| 2016-07-17 | Fixing printing of notations with several instances of a recursive pattern. | Hugo Herbelin | |
| 2016-07-17 | First step in adding printing for notations such as given in #4932. | Hugo Herbelin | |
| In particular, it becomes possible to have recursive patterns used shared by binders and terms. Currently limited by alpha-conversion issues (e.g. test2 from 4932.v is not reprinted). | |||
| 2016-07-17 | Fixing #4932 (anomaly when using binders as terms in recursive notations). | Hugo Herbelin | |
| This application was actually not anticipated. It is nice and was not too difficult to support. Design for pattern binders maybe to clarify. When seing pat(x1,..,xn) as a term, I just reused pat(x1,..,xn), but maybe it is worth using the variable aliasing the pattern, for more a concise notation. But at the same time, this means exposing the internal name of the alias which is not so elegant. | |||
| 2016-07-16 | Fixing a collision about the meta-variable ".." in recursive notations. | Hugo Herbelin | |
| This happens when recursive notations are used to define recursive notations. | |||
| 2016-07-13 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-07-13 | Fixing printing of evar name in an error message of instantiate. | Hugo Herbelin | |
| 2016-07-13 | Typo. | Hugo Herbelin | |
| 2016-07-13 | Makefile.dev: fix a typo in the 'logic' rule | Pierre Letouzey | |
| 2016-07-12 | Makefile.build: follow-up of commits by Matej on VERBOSE and READABLE_ML4 | Pierre Letouzey | |
| - With the ?= construction, we avoid warnings about undefined variables, while tolerating both 'make VERBOSE=1' and 'VERBOSE=1 make' - Some extra documentation and cleanup | |||
| 2016-07-12 | .gitignore: no more generated grammar/*.ml files | Pierre Letouzey | |
| 2016-07-12 | Makefile: no more .ml4.d hence no more rule to clean them | Pierre Letouzey | |
| 2016-07-12 | ".gitignore" update | Matej Kosik | |
| 2016-07-12 | removing ocamldoc-related syntax errors | Matej Kosik | |
| 2016-07-12 | expanding "make help" a little bit | Matej Kosik | |
| 2016-07-12 | Removing "READABLE_ML4=" from "Makefile.build" | Matej Kosik | |
| 2016-07-11 | Removing "VERBOSE=" from "Makefile.build" | Matej Kosik | |
| 2016-07-08 | Fixing the printing of unknown locations by adding a newline. | Pierre-Marie Pédrot | |
| 2016-07-08 | Adding a breaking space in warning names. | Pierre-Marie Pédrot | |
| 2016-07-08 | Remove spurious warnings about projections when requiring modules. | Pierre-Marie Pédrot | |
| 2016-07-08 | Add a few fixes in CHANGES that were forgotten. | Maxime Dénès | |
| We should really automate the generation of the log of fixes for CHANGES. | |||
| 2016-07-08 | Fix test file for #4858. | Maxime Dénès | |
| 2016-07-08 | Fixing #4906 (regression in printing an error message). | Hugo Herbelin | |
| 2016-07-08 | Typo in a comment of stdlib. | Hugo Herbelin | |
| 2016-07-08 | Update csdp.cache. | Maxime Dénès | |
| 2016-07-08 | Test file for #4858. | Maxime Dénès | |
| 2016-07-08 | Add test file for #4880. | Maxime Dénès | |
| 2016-07-08 | Update COPYRIGHT. | Maxime Dénès | |
| 2016-07-08 | Merge remote-tracking branch 'github/pr/243' into v8.5 | Maxime Dénès | |
| Was PR#243: fixing nsatz | |||
| 2016-07-07 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |