aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
Commit message (Expand)AuthorAge
* Fix Errors.out missing a dot...Gravatar Matthieu Sozeau2016-07-19
* Fixing printing of evar name in an error message of instantiate.Gravatar Hugo Herbelin2016-07-13
* Fixing subst.out after changing spacing in goal output (24a125b77).Gravatar Hugo Herbelin2016-05-04
* In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
* Remove extraneous space in coqtop/pg output (bug #4675).Gravatar Guillaume Melquiond2016-05-03
* Fixing output test Notations2.Gravatar Hugo Herbelin2016-04-22
* Fixing #4677 (collision of a global variable and of a local variableGravatar Hugo Herbelin2016-04-19
* Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
* Fix test suite after change in extraction.Gravatar Maxime Dénès2015-12-15
* Fixing output test Existentials.v after eec77191b.Gravatar Hugo Herbelin2015-11-07
* Fixing a bug in reporting ill-formed inductive.Gravatar Hugo Herbelin2015-10-22
* Fixing test-suiteGravatar Hugo Herbelin2015-10-11
* Fixing untimely unexpected warning "Collision between bound variables" (#4317).Gravatar Hugo Herbelin2015-10-11
* Refining 0c320e79ba30 in fixing interpretation of constr under bindersGravatar Hugo Herbelin2015-10-11
* Test for bug #4269.Gravatar Pierre-Marie Pédrot2015-09-15
* Update test-suite after 518049fe7.Gravatar Maxime Dénès2015-09-03
* Output test for bug #2169.Gravatar Pierre-Marie Pédrot2015-07-27
* Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8.Gravatar Maxime Dénès2015-06-24
* Do not display the status of monomorphic constants unless in universe-polymor...Gravatar Guillaume Melquiond2015-03-09
* Fix testsuite with respect to the new formatting of Fail messages.Gravatar Guillaume Melquiond2015-03-05
* Undo: back to 8.4 semantics (Close #3514)Gravatar Enrico Tassi2015-02-15
* Fixing name of evars in output test Notation.v.Gravatar Hugo Herbelin2015-01-12
* Adapted test file for About.Gravatar Pierre Courtieu2014-12-15
* About now accepts hypothesis names and goal selector.Gravatar Pierre Courtieu2014-12-15
* Tests for Searchxxx commands added and modified.Gravatar Pierre Courtieu2014-12-15
* Adapting output tests to current naming of evars, even if unclearGravatar Hugo Herbelin2014-11-11
* Consequence of changing the definition of Nat.shiftl and Nat.shiftr.Gravatar Hugo Herbelin2014-11-06
* Fixing clash in output test-suite Cases.Gravatar Hugo Herbelin2014-10-23
* Taking into account factorization of consecutive names of same typesGravatar Hugo Herbelin2014-10-23
* Fixing typo in output test Notations.Gravatar Hugo Herbelin2014-10-22
* Adapting output tests to the removal of the new token warning and toGravatar Hugo Herbelin2014-10-21
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Adapting output/Arguments_renaming continued.Gravatar Hugo Herbelin2014-10-03
* An evar name changed in output test.Gravatar Hugo Herbelin2014-10-02
* Adapting the output test Notations:Gravatar Hugo Herbelin2014-10-02
* Revert "test-suite: New names for vars but the expected invariant is preserved"Gravatar Hugo Herbelin2014-10-02
* Adapting output/Arguments_renaming.out after fixing printing ofGravatar Hugo Herbelin2014-10-02
* Adapting to naming of evars.Gravatar Hugo Herbelin2014-09-27
* Reductionops: (Co)Fixpoints are always refolded during iotaGravatar Pierre Boutillier2014-09-18
* Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10.Gravatar Hugo Herbelin2014-09-15
* Grammar: "avoiding to" isn't proper, eitherGravatar Jason Gross2014-08-25
* Upgrading output tests.Gravatar Hugo Herbelin2014-08-12
* Fixing output test-suite.Gravatar Pierre-Marie Pédrot2014-07-21
* cbn understand ! Arguments directiveGravatar Pierre Boutillier2014-06-04
* Fixing output test-suite: since universe polymorphism, the Print commandGravatar Pierre-Marie Pédrot2014-05-08
* Fixing #3293 (eta-expansion at "match" printing time was failingGravatar Hugo Herbelin2014-04-28
* Never suppress the typing constraint of bound variables whose name wasGravatar Pierre-Marie Pédrot2014-03-01
* test-suite: opaque term -> opaque proofGravatar Pierre Boutillier2014-02-28
* test-suite: New names for vars but the expected invariant is preservedGravatar Pierre Boutillier2014-02-28
* Fix output test-suite 'simpl tactic' -> 'reduction tactics'Gravatar Pierre Boutillier2014-02-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 21:38:21 +0000