aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* 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
* Fixing test-suite.Gravatar Pierre-Marie Pédrot2014-12-01
* Adding test for bug #3417.Gravatar Pierre-Marie Pédrot2014-11-30
* Test for bug #3485.Gravatar Pierre-Marie Pédrot2014-11-30
* Test for bug #3487.Gravatar Pierre-Marie Pédrot2014-11-30
* Test of bug #3682.Gravatar Pierre-Marie Pédrot2014-11-30
* Fix test flags for fake_ideGravatar Enrico Tassi2014-11-27
* Bug #3804 is actually closed (thanks to Jason Gross for the notification).Gravatar Xavier Clerc2014-11-25
* Tweak some test cases.Gravatar Xavier Clerc2014-11-25
* Adapting to current semantics of "simpl non-evaluable-cst"Gravatar Hugo Herbelin2014-11-25
* Experimenting using unification when matching evar/meta free subtermsGravatar Hugo Herbelin2014-11-25
* Adding test for bug #3248.Gravatar Pierre-Marie Pédrot2014-11-24
* Pass around information on the use of template polymorphism forGravatar Matthieu Sozeau2014-11-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 17:02:27 +0000