| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Simplifying code in evar generation. |  Pierre-Marie Pédrot | 2016-08-04 |
| | | | | | | | | We remove in particular a dubious use of an environment in fresh name generation. The code was using the wrong environment in a function only depending on the rel context which was resetted most of the time. This might change the generated names in extremely rare occurences. | ||
| * | Exporting the renaming API for evar declaration. | Pierre-Marie Pédrot | 2016-08-04 |
| | | |||
| * | Embedding the pretyping environment in a dummy record. | Pierre-Marie Pédrot | 2016-08-04 |
| | | |||
| * | Merge remote-tracking branch 'gforge/v8.5' into v8.6 |  Matthieu Sozeau | 2016-07-29 |
| |\ | |||
| | * | Update CHANGES about #3886 bugfix |  Matthieu Sozeau | 2016-07-29 |
| | | | |||
| | * | Fix bug #3886, generation of obligations of fixes | Matthieu Sozeau | 2016-07-29 |
| | | | | | | | | | This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1 | ||
| | * | Fix #4769, univ poly and elim schemes in sections | Matthieu Sozeau | 2016-07-29 |
| | | | |||
| * | | COMMENT: moving misplaced comment where it belongs |  Matej Kosik | 2016-07-29 |
| | | | |||
| * | | Adding a flag in CoqIDE to configure UNIX/Windows line ending. | Pierre-Marie Pédrot | 2016-07-26 |
| | | | | | | | | | Fixes both bugs #4924 and #4437. | ||
| * | | restore compatibility with gallium's camlp4 (broken by commit 8e07227c) |  Pierre Letouzey | 2016-07-26 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Apparently, in camlp4 (unlike camlp5) : - Something like "[ kwd = IDENT "foobar" -> .... kwd ... ]" produces a kwd of type token instead of string (which sounds reasonable ?). For now, I've replaced kwd by the explicit strings. Not so nice, but works with both camlp4 and camlp5 - A quotation of the form "let obj = ... in bar; baz" is not interpreted in the usual OCaml way, but rather as "(let obj = ... in bar); baz". Let's use instead "let obj = ... in let () = bar in baz", which works fine. | ||
| | * | Update CHANGES about critical bugfix and others | Matthieu Sozeau | 2016-07-26 |
| | | | |||
| | * | Merge branch 'bug4754' into v8.5 | Matthieu Sozeau | 2016-07-26 |
| | |\ | |||
| | | * | Fix bug #4754, allow conversion problems to remain | Matthieu Sozeau | 2016-07-26 |
| | |/ | | | | | | | | | when checking that the rewrite relation is homogeneous in setoid_rewrite. | ||
| * | | Merge remote-tracking branch 'gforge/v8.5' into v8.6 | Matthieu Sozeau | 2016-07-26 |
| |\| | |||
| | * | Merge branch 'bug4876' into v8.5 | Matthieu Sozeau | 2016-07-26 |
| | |\ | |||
| * | \ | Merge remote-tracking branch 'github/bug4679' into v8.6 | Matthieu Sozeau | 2016-07-25 |
| |\ \ \ | |||
| | | | * | Fix bug #4876: critical bug in guard condition checker. | Matthieu Sozeau | 2016-07-25 |
| | | |/ | |||
| | * | | Fix bug #4679, weakened setoid_rewrite unification | Matthieu Sozeau | 2016-07-21 |
| | | | | | | | | | | | | | | | | It should use evar instantiations eagerly during unification of the lhs of the lemma, as in 8.4. | ||
| * | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-07-20 |
| |\ \ \ | |/ / |/| / | |/ | |||
| | * | Update CHANGES | Matthieu Sozeau | 2016-07-20 |
| | | | |||
| | * | Fix bug #4780: universe leak in letin_tac | Matthieu Sozeau | 2016-07-20 |
| | | | |||
| * | | Update CHANGES | Matthieu Sozeau | 2016-07-20 |
| | | | |||
| * | | Fix bug #4780: universe leak in letin_tac | Matthieu Sozeau | 2016-07-20 |
| | | | |||
| | * | Fix Errors.out missing a dot... | 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 | 2016-07-19 |
| | | | | | | | | | | | | | | | | | | | | | - 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. | ||
| * | | Taking into account binding patterns when agglutinating sequences of binders. | Hugo Herbelin | 2016-07-19 |
| | | | | | | | | | | | Supporting accordingly printing of sequences of binders including binding patterns. | ||
| * | | 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 | 2016-07-19 |
| | | | | | | | | | (In agreement with Daniel.) | ||
| * | | 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 | 2016-07-19 |
| | | | | | | | | | | | | | | | | | | | | | | | 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. | ||
| * | | Fixing extra returns in top_printers.ml (msg_notice not same semantics as pp). | Hugo Herbelin | 2016-07-19 |
| | | | |||
| * | | A new step on using alpha-conversion in printing notations. | Hugo Herbelin | 2016-07-18 |
| | | | | | | | | | | | | | | | 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). | ||
| * | | Replacing deprecated Implicit Arguments in prelude. |  Maxime Dénès | 2016-07-18 |
| | | | | | | | | | Was triggering a deprecation warning. | ||
| * | | Remove the swap tactic from the prelude. | Maxime Dénès | 2016-07-18 |
| | | | | | | | | | | | It was anyway unusable due to a parsing conflict with the swap operator on goals. Was triggering a warning when compiling the prelude. | ||
| * | | 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-18 |
| | | | |||
| * | | 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 | 2016-07-17 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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) ..) ..). | ||
| * | | Fixing a bug in recognizing a recursive pattern of notations | Hugo Herbelin | 2016-07-17 |
| | | | | | | | | | immediately in the scope of another recursive pattern. | ||
| * | | 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 | 2016-07-17 |
| | | | | | | | | | | | | | | | | | 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). | ||
| * | | Fixing #4932 (anomaly when using binders as terms in recursive notations). | Hugo Herbelin | 2016-07-17 |
| | | | | | | | | | | | | | | | | | | | | | | | 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. | ||
| * | | Fixing a collision about the meta-variable ".." in recursive notations. | Hugo Herbelin | 2016-07-16 |
| | | | | | | | | | | | This happens when recursive notations are used to define recursive notations. | ||
| * | | 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-13 |
| | | | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |