| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-17 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-15 | Fix test suite after change in extraction. | Maxime Dénès | |
| 2015-12-05 | Using x in output test-suite Cases.v (cosmetic). | Hugo Herbelin | |
| 2015-11-15 | Fixing output test Cases.v. | Pierre-Marie Pédrot | |
| Not sure if this is really what is expected though. | |||
| 2015-11-10 | Updating test-suite after Bracketing Last Introduction Pattern set by | Hugo Herbelin | |
| default. Interestingly, there is an example where it makes the rest of the proof less natural. Goal forall x y:Z, ... intros [y|p1[|p2|p2]|p1[|p2|p2]]. where case analysis on y is not only in the 2nd and 3rd case, is not anymore easy to do. Still, I find the bracketing of intro-patterns a natural property, and its generalization in all situations a natural expectation for uniformity. So, what to do? The following is e.g. not as compact and "one-shot": intros [|p1|p1]; [intros y|intros [|p2|p2] ..]. | |||
| 2015-11-10 | Merge origin/v8.5 into trunk | Hugo Herbelin | |
| Did some manual merge in tactics/tactics.ml. | |||
| 2015-11-08 | Adapting output test inference.v after c23f0cab6 (experimenting | Hugo Herbelin | |
| printing the type of the defined term of a LetIn). | |||
| 2015-11-07 | Fixing output test Existentials.v after eec77191b. | Hugo Herbelin | |
| 2015-10-22 | Fixing a bug in reporting ill-formed inductive. | Hugo Herbelin | |
| Was introduced in b06d3badb (15 Jul 2015). | |||
| 2015-10-11 | Fixing test-suite | Hugo Herbelin | |
| 2015-10-11 | Fixing untimely unexpected warning "Collision between bound variables" (#4317). | Hugo Herbelin | |
| 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. | |||
| 2015-10-11 | Refining 0c320e79ba30 in fixing interpretation of constr under binders | Hugo Herbelin | |
| 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. | |||
| 2015-09-15 | Test for bug #4269. | Pierre-Marie Pédrot | |
| 2015-09-03 | Update test-suite after 518049fe7. | Maxime Dénès | |
| "Fetching opaque proofs" notices are not printed by default anymore. | |||
| 2015-07-27 | Output test for bug #2169. | Pierre-Marie Pédrot | |
| 2015-06-24 | Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8. | Maxime Dénès | |
| 2015-03-09 | Do not display the status of monomorphic constants unless in ↵ | Guillaume Melquiond | |
| universe-polymorphism mode. | |||
| 2015-03-05 | Fix testsuite with respect to the new formatting of Fail messages. | Guillaume Melquiond | |
| 2015-02-15 | Undo: back to 8.4 semantics (Close #3514) | Enrico Tassi | |
| Only tactics are taken into account. | |||
| 2015-01-12 | Fixing name of evars in output test Notation.v. | Hugo Herbelin | |
| 2014-12-15 | 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-11-11 | Adapting output tests to current naming of evars, even if unclear | Hugo Herbelin | |
| where it will eventually stabilize. | |||
| 2014-11-06 | Consequence of changing the definition of Nat.shiftl and Nat.shiftr. | Hugo Herbelin | |
| 2014-10-23 | Fixing clash in output test-suite Cases. | Hugo Herbelin | |
| 2014-10-23 | Taking into account factorization of consecutive names of same types | Hugo Herbelin | |
| 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. | |||
| 2014-10-22 | Fixing typo in output test Notations. | Hugo Herbelin | |
| 2014-10-21 | Adapting output tests to the removal of the new token warning and to | Hugo Herbelin | |
| the printing of the context of open evars in Check. | |||
| 2014-10-20 | A patch for printing "match" when constructors are defined with let-in | Hugo Herbelin | |
| 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. | |||
| 2014-10-03 | Adapting output/Arguments_renaming continued. | Hugo Herbelin | |
| 2014-10-02 | An evar name changed in output test. | Hugo Herbelin | |
| 2014-10-02 | Adapting the output test Notations: | Hugo Herbelin | |
| - unbound variables in notation are allowed, forcing only parsing mode - plus and mult are now themselves abbreviations - evars are named | |||
| 2014-10-02 | Revert "test-suite: New names for vars but the expected invariant is preserved" | Hugo Herbelin | |
| 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. | |||
| 2014-10-02 | Adapting output/Arguments_renaming.out after fixing printing of | Hugo Herbelin | |
| constants which without a @ would have a maximally inserted implicit argument. | |||
| 2014-09-27 | Adapting to naming of evars. | Hugo Herbelin | |
| 2014-09-18 | Reductionops: (Co)Fixpoints are always refolded during iota | Pierre Boutillier | |
| 2014-09-15 | Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10. | Hugo Herbelin | |
| 2014-08-25 | Grammar: "avoiding to" isn't proper, either | Jason Gross | |
| 2014-08-12 | Upgrading output tests. | Hugo Herbelin | |
| 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 | |||
| 2014-07-21 | Fixing output test-suite. | Pierre-Marie Pédrot | |
| 2014-06-04 | cbn understand ! Arguments directive | Pierre Boutillier | |
| Of course, this is an under approximation of the expected behavior : unfolding a constant iff a leaf of its underlying split-tree is reached. | |||
| 2014-05-08 | Fixing output test-suite: since universe polymorphism, the Print command | Pierre-Marie Pédrot | |
| shows the polymorphism status of the term. | |||
| 2014-04-28 | Fixing #3293 (eta-expansion at "match" printing time was failing | Hugo Herbelin | |
| because of let-in's interpreted as being part of the expansion). | |||
| 2014-03-01 | Never suppress the typing constraint of bound variables whose name was | Pierre-Marie Pédrot | |
| reserved with Implicit Type. | |||
| 2014-02-28 | 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 | |
| 2013-12-19 | test-suite/output/Notations : evar number change | Pierre Boutillier | |
| 2013-12-02 | Test suite: update output reference. | xclerc | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |