| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-10-09 | Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for ↵ | Maxime Dénès | |
| printing-ony Notations | |||
| 2017-10-04 | Merge PR #1078: Report missing arguments in error message | Maxime Dénès | |
| 2017-10-04 | Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial). | Maxime Dénès | |
| 2017-09-25 | BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations | Paul Steckler | |
| 2017-09-21 | Report missing arguments in error message | Tej Chajed | |
| Augment the "Illegal tactic application" error message with the number of extra arguments passed. Fixes BZ#5753. | |||
| 2017-09-19 | Fixing bug #5741 (anomaly in info_trivial). | Hugo Herbelin | |
| The bug was introduced in 1559f73. | |||
| 2017-09-19 | Don't lose names in UState.universe_context. | Gaëtan Gilbert | |
| We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it. | |||
| 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-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 | 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-08-29 | Adding a test for #5569 (warning about skipping spaces). | Hugo Herbelin | |
| The two previous commits make the warning irrelevant and useless. | |||
| 2017-08-29 | A little reorganization of notations + a fix to #5608. | Hugo Herbelin | |
| - Formerly, notations such as "{ A } + { B }" were typically split into "{ _ }" and "_ + _". We keep the split only for parsing, which is where it is really needed, but not anymore for interpretation, nor printing. - As a consequence, one notation string can give rise to several grammar entries, but still only one printing entry. - As another consequence, "{ A } + { B }" and "A + { B }" must be reserved to be used, which is after all the natural expectation, even if the sublevels are constrained. - We also now keep the information "is ident", "is binder" in the "key" characterizing the level of a notation. | |||
| 2017-08-21 | Ensuring all .v files end with a newline to make "sed -i" work better on them. | Hugo Herbelin | |
| 2017-08-06 | Print names of all open blocks | Tej Chajed | |
| Fixes bug 5597. | |||
| 2017-08-01 | Merge PR #834: Adding support for recursive notations of the form "x , .. , ↵ | Maxime Dénès | |
| y , z". | |||
| 2017-07-26 | Fix TypeclassDebug.out after conflicting PR merges | Matthieu Sozeau | |
| 2017-07-26 | Adding support for recursive notations of the form "x , .. , y , z". | Hugo Herbelin | |
| Since camlp5 parses from left, the last ", z" was parsed as part of an arbitrary long list of "x1 , .. , xn" and a syntax error was raised since an extra ", z" was still expected. We support this by translating "x , .. , y , z" into "x , y , .. , z" and reassembling the arguments appropriately after parsing. | |||
| 2017-07-20 | Merge PR #869: Enforce alternating separators in typeclass debug output | Maxime Dénès | |
| 2017-07-12 | format pairs of items for pr_depth to get alternating separators | Paul Steckler | |
| eval thunks once in prlist_sep_lastsep, make code clearer add typeclass debug output test | |||
| 2017-07-11 | Deprecate options that were introduced for compatibility with 8.5. | Théo Zimmermann | |
| 2017-07-07 | Merge PR #863: Fixing environment in warning "Projection value has no head ↵ | Maxime Dénès | |
| constant". | |||
| 2017-07-07 | Fixing environment in warning "Projection value has no head constant". | Hugo Herbelin | |
| Delaying also some computation needed for printing to the time of really printing it. | |||
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-06-23 | Add tests for handling of warnings | Tej Chajed | |
| 2017-06-14 | Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match"). | Maxime Dénès | |
| 2017-06-14 | Prelude : no more autoload of plugins extraction and recdef | Pierre Letouzey | |
| The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted. | |||
| 2017-06-13 | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | Pierre Letouzey | |
| See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude. | |||
| 2017-06-09 | Fix Bug #5568, no dup notation warnings on repeated module imports | Paul Steckler | |
| 2017-06-09 | A fix to #5414 (ident bound by ltac names now known for "match"). | Hugo Herbelin | |
| Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let". | |||
| 2017-06-08 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-06-02 | Merge PR#647: [emacs] [toplevel] Make emacs flag local to the toplevel. | Maxime Dénès | |
| 2017-06-01 | [emacs] [toplevel] Make emacs flag local to the toplevel. | Emilio Jesus Gallego Arias | |
| We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel. | |||
| 2017-06-01 | Merge PR#694: Fixing #5523 (missing support for complex constructions in ↵ | Maxime Dénès | |
| recursive notations) (bis) | |||
| 2017-05-31 | Fixing a too lax constraint for finding recursive binder part of a notation. | Hugo Herbelin | |
| This was preventing to work examples such as: Notation "[ x ; .. ; y ; z ]" := ((x,((fun u => u), .. (y,(fun u =>u,z)) ..))). | |||
| 2017-05-30 | Support for using type information to infer more precise evar sources. | Hugo Herbelin | |
| This allows a better control on the name to give to an evar and, in particular, to address the issue about naming produced by "epose proof" in one of the comment of Zimmi48 at PR #248 (see file names.v). Incidentally updating output of Show output test (evar numbers shifted). | |||
| 2017-05-29 | Merge PR#546: Fix for bug #4499 and other minor related bugs | Maxime Dénès | |
| 2017-05-28 | Merge PR#679: Bug 5546, qualify datatype constructors when needed in Show Match | Maxime Dénès | |
| 2017-05-26 | Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if ↵ | Maxime Dénès | |
| printing only | |||
| 2017-05-25 | add Show test with -emacs flag | Paul Steckler | |
| 2017-05-25 | Bug 5546, qualify datatype constructors when needed | Paul Steckler | |
| 2017-05-23 | Merge PR#661: Added a test for #4765 (an example of printing abbreviation ↵ | Maxime Dénès | |
| with binders) | |||
| 2017-05-23 | Merge PR#657: [test-suite] Add tests for goal printing. | Maxime Dénès | |
| 2017-05-20 | Added a test for #4765 (an example of printing abbreviation with binders). | Hugo Herbelin | |
| 2017-05-20 | [test-suite] Add tests for goal printing. | Emilio Jesus Gallego Arias | |
| - https://coq.inria.fr/bugs/show_bug.cgi?id=5529 - https://coq.inria.fr/bugs/show_bug.cgi?id=5537 See also PR #640 | |||
| 2017-05-19 | add test for Show with -emacs, bug 5535 | Paul Steckler | |
| 2017-05-17 | A fix for #5390 (a useful error on used introduction names was masked). | Hugo Herbelin | |
| With the "apply in" introduction pattern, and the backtrack possibly done in "apply" over the components of conjunctions (descend_in_conjunctions), the reasons for failing might have different sources. We give priority to the detection of used names over other (unification) errors so that an error there is not masked in the backtracking made by descend_in_conjunctions. Of course, the question of what best unification error to give in the presence of backtracking is still open. | |||
| 2017-05-17 | Fixing bug #5526,allow nonlinear variables in Notation patterns | Paul Steckler | |
| 2017-05-17 | Merge PR#457: Adding an even more compact goal hyps mode. | Maxime Dénès | |
| 2017-05-17 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-05-16 | Simplified compaction criterion + tests. | Pierre Courtieu | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |