| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix Errors.out missing a dot... |  Matthieu Sozeau | 2016-07-19 |
| | | |||
| * | Fixing printing of evar name in an error message of instantiate. |  Hugo Herbelin | 2016-07-13 |
| | | |||
| * | Fixing subst.out after changing spacing in goal output (24a125b77). | Hugo Herbelin | 2016-05-04 |
| | | |||
| * | In Regular Subst Tactic mode, ensure that the order of hypotheses is | Hugo Herbelin | 2016-05-03 |
| | | | | | | | | | | | | | | | | preserved, which is a source of incompatibilities w.r.t. released 8.5 but which looks to me to be the only possible canonical behavior. This is I believe a better behavior than the Regular Subst Tactic behavior in the released 8.5 and 8.5pl1. There, the order of hypotheses in which substitutions happened was respected, but their interleaving with other hypotheses was not respected. So, I consider this to be a fix to the "Regular Subst Tactic" mode. Also added a more detailed "specification" of the "Regular" behavior of "subst" in the reference manual. | ||
| * | Remove extraneous space in coqtop/pg output (bug #4675). |  Guillaume Melquiond | 2016-05-03 |
| | | |||
| * | Fixing output test Notations2. | Hugo Herbelin | 2016-04-22 |
| | | |||
| * | Fixing #4677 (collision of a global variable and of a local variable | Hugo Herbelin | 2016-04-19 |
| | | | | | | while eta-expanding a notation) + a more serious variant of it (alpha-conversion incorrect wrt eta-expansion). | ||
| * | Do not give a name to anonymous evars anymore. See bug #4547. |  Pierre-Marie Pédrot | 2016-02-13 |
| | | | | | | | | | The current solution may not be totally ideal though. We generate names for anonymous evars on the fly at printing time, based on the Evar_kind data they are wearing. This means in particular that the printed name of an anonymous evar may change in the future because some unrelate evar has been solved or introduced. | ||
| * | Fix test suite after change in extraction. |  Maxime Dénès | 2015-12-15 |
| | | |||
| * | Fixing output test Existentials.v after eec77191b. | Hugo Herbelin | 2015-11-07 |
| | | |||
| * | Fixing a bug in reporting ill-formed inductive. | Hugo Herbelin | 2015-10-22 |
| | | | | | Was introduced in b06d3badb (15 Jul 2015). | ||
| * | Fixing test-suite | Hugo Herbelin | 2015-10-11 |
| | | |||
| * | Fixing untimely unexpected warning "Collision between bound variables" (#4317). | Hugo Herbelin | 2015-10-11 |
| | | | | | | | Collecting the bound variables is now done on the glob_constr, before interpretation, so that only variables given explicitly by the user are used for binding bound variables. | ||
| * | Refining 0c320e79ba30 in fixing interpretation of constr under binders | Hugo Herbelin | 2015-10-11 |
| | | | | | | | | which was broken after it became possible to have binding names themselves bound to ltac variables (2fcc458af16b). Interpretation was corrected, but error message was damaged. | ||
| * | Test for bug #4269. | Pierre-Marie Pédrot | 2015-09-15 |
| | | |||
| * | Update test-suite after 518049fe7. | Maxime Dénès | 2015-09-03 |
| | | | | | "Fetching opaque proofs" notices are not printed by default anymore. | ||
| * | Output test for bug #2169. | Pierre-Marie Pédrot | 2015-07-27 |
| | | |||
| * | Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8. | Maxime Dénès | 2015-06-24 |
| | | |||
| * | Do not display the status of monomorphic constants unless in ↵ | Guillaume Melquiond | 2015-03-09 |
| | | | | | universe-polymorphism mode. | ||
| * | Fix testsuite with respect to the new formatting of Fail messages. | Guillaume Melquiond | 2015-03-05 |
| | | |||
| * | Undo: back to 8.4 semantics (Close #3514) |  Enrico Tassi | 2015-02-15 |
| | | | | | Only tactics are taken into account. | ||
| * | Fixing name of evars in output test Notation.v. | Hugo Herbelin | 2015-01-12 |
| | | |||
| * | Adapted test file for About. |  Pierre Courtieu | 2014-12-15 |
| | | |||
| * | About now accepts hypothesis names and goal selector. | Pierre Courtieu | 2014-12-15 |
| | | |||
| * | Tests for Searchxxx commands added and modified. | Pierre Courtieu | 2014-12-15 |
| | | |||
| * | Adapting output tests to current naming of evars, even if unclear | Hugo Herbelin | 2014-11-11 |
| | | | | | where it will eventually stabilize. | ||
| * | Consequence of changing the definition of Nat.shiftl and Nat.shiftr. | Hugo Herbelin | 2014-11-06 |
| | | |||
| * | Fixing clash in output test-suite Cases. | Hugo Herbelin | 2014-10-23 |
| | | |||
| * | Taking into account factorization of consecutive names of same types | Hugo Herbelin | 2014-10-23 |
| | | | | | | | | | | | | | in goal context. Note: printing of a declaration was previously done in the context made of the preceding segment of hypotheses, while now it is made in the full context of all hyps (those coming before and after the hyp being printed). As a consequence, constants which could be confused with a variable in the context are now always qualified even if the conflicting variable name is coming later. But why not, that looks somehow more uniform like this. | ||
| * | Fixing typo in output test Notations. | Hugo Herbelin | 2014-10-22 |
| | | |||
| * | Adapting output tests to the removal of the new token warning and to | Hugo Herbelin | 2014-10-21 |
| | | | | | the printing of the context of open evars in Check. | ||
| * | A patch for printing "match" when constructors are defined with let-in | Hugo Herbelin | 2014-10-20 |
| | | | | | | | | | | | | but the internal representation dropped let-in. Ideally, the internal representation of the "match" should use contexts for the predicate and the branches. This would however be a rather significant change. In the meantime, just a hack. To do, there is still an extra @ in the constructor name that does not need to be there. | ||
| * | Adapting output/Arguments_renaming continued. | Hugo Herbelin | 2014-10-03 |
| | | |||
| * | An evar name changed in output test. | Hugo Herbelin | 2014-10-02 |
| | | |||
| * | Adapting the output test Notations: | Hugo Herbelin | 2014-10-02 |
| | | | | | | | - unbound variables in notation are allowed, forcing only parsing mode - plus and mult are now themselves abbreviations - evars are named | ||
| * | Revert "test-suite: New names for vars but the expected invariant is preserved" | Hugo Herbelin | 2014-10-02 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit cc06ffe3df0ecc023ad046a085b0751ed4161cbf. Going back to the convention of naming bound variables in hypotheses of the goal as in 8.4. My arguments for the revert are: - apply ... with (id:=...) would have to be changed too, then possibly breaking the compatibility - the naming became dependent of the order of variables as in x:nat H:forall x0, x0=0 ===== goal but H:forall x, x=0 x:nat ===== goal Accordingly, this is all a matter of convention, since the meaning of bindings is anyway the same in both cases. | ||
| * | Adapting output/Arguments_renaming.out after fixing printing of | Hugo Herbelin | 2014-10-02 |
| | | | | | | constants which without a @ would have a maximally inserted implicit argument. | ||
| * | Adapting to naming of evars. | Hugo Herbelin | 2014-09-27 |
| | | |||
| * | Reductionops: (Co)Fixpoints are always refolded during iota |  Pierre Boutillier | 2014-09-18 |
| | | |||
| * | Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10. | Hugo Herbelin | 2014-09-15 |
| | | |||
| * | Grammar: "avoiding to" isn't proper, either |  Jason Gross | 2014-08-25 |
| | | |||
| * | Upgrading output tests. | Hugo Herbelin | 2014-08-12 |
| | | | | | | | | | | | | | output/Arguments.v output/ArgumentsScope.v output/Arguments_renaming.v output/Cases.v output/Implicit.v output/PrintInfos.v output/TranspModType.v Main changes: monomorphic -> not universe polymorphic, Peano vs Nat | ||
| * | Fixing output test-suite. | Pierre-Marie Pédrot | 2014-07-21 |
| | | |||
| * | cbn understand ! Arguments directive | Pierre Boutillier | 2014-06-04 |
| | | | | | | Of course, this is an under approximation of the expected behavior : unfolding a constant iff a leaf of its underlying split-tree is reached. | ||
| * | Fixing output test-suite: since universe polymorphism, the Print command | Pierre-Marie Pédrot | 2014-05-08 |
| | | | | | shows the polymorphism status of the term. | ||
| * | Fixing #3293 (eta-expansion at "match" printing time was failing | Hugo Herbelin | 2014-04-28 |
| | | | | | because of let-in's interpreted as being part of the expansion). | ||
| * | Never suppress the typing constraint of bound variables whose name was | Pierre-Marie Pédrot | 2014-03-01 |
| | | | | | reserved with Implicit Type. | ||
| * | test-suite: opaque term -> opaque proof | Pierre Boutillier | 2014-02-28 |
| | | |||
| * | test-suite: New names for vars but the expected invariant is preserved | Pierre Boutillier | 2014-02-28 |
| | | |||
| * | Fix output test-suite 'simpl tactic' -> 'reduction tactics' | Pierre Boutillier | 2014-02-28 |
| | | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |