aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Test for bug #3798.Gravatar Pierre-Marie Pédrot2015-01-25
* There was one more universe needed due to the use of now non-universe-polymor...Gravatar Matthieu Sozeau2015-01-18
* Back to 4 expected universes.Gravatar Matthieu Sozeau2015-01-17
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Revert "Adapting two files from test-suite to now forbidden Require's in modu...Gravatar Maxime Dénès2015-01-17
* Revert "Update test for #3363 now that Require is forbidden inside modules."Gravatar Maxime Dénès2015-01-17
* Revert "Fix files in test-suite having to do with Require inside modules."Gravatar Maxime Dénès2015-01-17
* Univs: Fix alias computation for VMs, computation of normal form ofGravatar Matthieu Sozeau2015-01-17
* Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"Gravatar Matthieu Sozeau2015-01-16
* TCs: Properly handle Hint Extern with conclusions of the form _ -> _Gravatar Matthieu Sozeau2015-01-13
* Fix test-suite file, we were testing that no anomaly was raisedGravatar Matthieu Sozeau2015-01-13
* Fix files in test-suite having to do with Require inside modules.Gravatar Maxime Dénès2015-01-12
* Update headers.Gravatar Maxime Dénès2015-01-12
* Update test for #3363 now that Require is forbidden inside modules.Gravatar Maxime Dénès2015-01-12
* Fixing name of evars in output test Notation.v.Gravatar Hugo Herbelin2015-01-12
* Extraction: discard code unnecessary to fulfill a module signatureGravatar Pierre Letouzey2015-01-11
* STM: fix handling of side effects in vio2voGravatar Enrico Tassi2015-01-09
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
* Fixing test for bug #2830.Gravatar Pierre-Marie Pédrot2015-01-06
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
* Adapting two files from test-suite to now forbidden Require's in modules.Gravatar Hugo Herbelin2015-01-04
* Fixing #3896 (incorrect sigma given to printer).Gravatar Hugo Herbelin2015-01-03
* Fixing #3895 (thanks to PMP for diagnosis).Gravatar Hugo Herbelin2015-01-03
* An optimization in the use of unification candidates so as to get theGravatar Hugo Herbelin2015-01-01
* Fixing #3892: Ensure that notation variables do not capture namesGravatar Hugo Herbelin2014-12-30
* include test-suite/coqchk in the summary logGravatar Enrico Tassi2014-12-27
* new test for coqchkGravatar Enrico Tassi2014-12-26
* Better doc and a few fixes for Proof using.Gravatar Enrico Tassi2014-12-19
* Fixing wrong notation level in #3295.Gravatar Hugo Herbelin2014-12-19
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
* Future: blocking by defaultGravatar Enrico Tassi2014-12-17
* #3828 is solved.Gravatar Hugo Herbelin2014-12-16
* Moving #2447 (congruence) to fixed.Gravatar Hugo Herbelin2014-12-16
* Test for #3654.Gravatar Hugo Herbelin2014-12-16
* fix bug #2447 in congruenceGravatar Pierre Corbineau2014-12-16
* Adapted test file for About.Gravatar Pierre Courtieu2014-12-15
* Tests for #3848 and #3854.Gravatar Hugo Herbelin2014-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
* Two fixes in unification (bugs #3782 and #3709)Gravatar Matthieu Sozeau2014-12-12
* Test suite: keep message in sync with actual file deletions.Gravatar Xavier Clerc2014-12-11
* New reproduction cases for the test suite.Gravatar Xavier Clerc2014-12-11
* Fixing orientation of postponed subtyping problems.Gravatar Hugo Herbelin2014-12-10
* typoGravatar Enrico Tassi2014-12-10
* test-suite: few tests for ".v -> .vi -> .vo" compilation chainGravatar Enrico Tassi2014-12-10
* Improving evar restriction (this is a risky change, as I remember aGravatar Hugo Herbelin2014-12-07
* Commits on evar-evar unification fixed HoTT_coq_106 and improved theGravatar Hugo Herbelin2014-12-05
* Take benefit of improved name preservation of evars in e2fa65fcc.Gravatar Hugo Herbelin2014-12-04
* Updading test-suite.Gravatar Hugo Herbelin2014-12-03
* When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' ifGravatar Hugo Herbelin2014-12-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 04:21:20 +0000