aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
...
| | | * | | | | Adding tests for chained abstract tactics.Gravatar Pierre-Marie Pédrot2017-04-04
| | |/ / / / / | |/| | | | |
* | | | | | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\| | | | | |
| | | | * | | Test file for #5435: [Eval native_compute in] raises anomaly.Gravatar Maxime Dénès2017-04-04
| | | | | |/ | | | | |/|
| * | | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-03
| |\ \ \ \ \ | | | |_|/ / | | |/| | |
| | * | | | Instances should obey universe binders even when defined by tactics.Gravatar Gaetan Gilbert2017-04-03
| * | | | | Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
| |\ \ \ \ \
| | | * | | | Add test file for #4957.Gravatar Maxime Dénès2017-04-03
| * | | | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-30
| |\ \ \ \ \ \ | | | |/ / / / | | |/| | | |
| | * | | | | Run non-tactic comands without resilient_commandGravatar Tej Chajed2017-03-29
* | | | | | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\| | | | | |
| | | * | | | Applying same convention as in Definition for printing type in a let in.Gravatar Hugo Herbelin2017-03-24
| | |/ / / / | |/| | | |
| | | | * | Supporting arbitrary binders in record fields, including e.g. patterns.Gravatar Hugo Herbelin2017-03-23
| | | | * | A test checking for non-collision of name in irrefutable patterns.Gravatar Hugo Herbelin2017-03-23
| | |_|/ / | |/| | |
| * | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
| |\| | |
| | * | | Merge PR#507: Intern names bound in match patternsGravatar Maxime Dénès2017-03-23
| | |\ \ \
| | | * | | Intern names bound in match patternsGravatar Tej Chajed2017-03-23
| * | | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
| |\| | | |
| * | | | | Make IZR use a compact representation of integers.Gravatar Guillaume Melquiond2017-03-22
| | * | | | funind: Ignore missing info for current functionGravatar Tej Chajed2017-03-22
| | |/ / /
| * | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-03-22
| |\| | |
| * | | | [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | * | | Merge PR#429: Don't require printing-only notation to be productiveGravatar Maxime Dénès2017-03-17
| | |\ \ \
| * | | | | Report missing tactic arguments in error messageGravatar Tej Chajed2017-03-14
| | * | | | Merge PR#359: Fix bug 4969, autoapply was not tagging shelved subgoals correc...Gravatar Maxime Dénès2017-03-10
| | |\ \ \ \
| | | | | * | Farewell decl_modeGravatar Enrico Tassi2017-03-07
| | |_|_|/ / | |/| | | |
| * | | | | Merge PR#395: Allow hintdb to be parameters in a Ltac definition orGravatar Maxime Dénès2017-02-27
| |\ \ \ \ \
| | | | | | * Fixing a little bug in using the "where" clause for inductive types.Gravatar Hugo Herbelin2017-02-23
| * | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-22
| |\ \ \ \ \ \ | | | |/ / / / | | |/| | | |
| * | | | | | Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
| | | | | * | reject notations that are both 'only printing' and 'only parsing'Gravatar Ralf Jung2017-02-16
| | | | | * | don't require printing-only notation to be productiveGravatar Ralf Jung2017-02-16
| | | |_|/ / | | |/| | |
* | | | | | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\| | | | |
* | | | | | Quick hack to fix interpretation of patterns in Ltac.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | | | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| * | | | | Merge PR#253: Sort Search results by relevanceGravatar Maxime Dénès2017-02-14
| |\ \ \ \ \
| | * | | | | Test-suite: output of SearchGravatar Arnaud Spiwack2017-02-14
| |/ / / / / |/| | | | |
| | * | | | Fixing bug #5346 (an unimplemented application of 'pat).Gravatar Hugo Herbelin2017-02-09
| | | * | | Add test-suite files for hintdb variables in Ltac.Gravatar Théo Zimmermann2017-02-07
| | |/ / / | |/| | |
| * | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
| |\| | |
| | * | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-02-01
| | |\ \ \ | | | | |/ | | | |/|
| | | * | Fixing #5311 (anomaly on unexpected intro pattern).Gravatar Hugo Herbelin2017-01-31
| | * | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-01-23
| | |\| |
| | | * | Fixing unification regression #5323.Gravatar Hugo Herbelin2017-01-23
| | * | | Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins).Gravatar Hugo Herbelin2017-01-22
| | | * | Fixing a little bug in printing cofix with no arguments.Gravatar Hugo Herbelin2017-01-05
| * | | | Fixing #5277 (Scheme Equality not robust wrt choice of names).Gravatar Hugo Herbelin2016-12-22
| * | | | Fixing injection in the presence of let-in in constructors.Gravatar Hugo Herbelin2016-12-22
| * | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
| |\| | |
| | * | | Merge remote-tracking branch 'github/pr/366' into v8.6Gravatar Maxime Dénès2016-12-04
| | |\ \ \
| | * \ \ \ Merge remote-tracking branch 'github/pr/378' into v8.6Gravatar Maxime Dénès2016-12-04
| | |\ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 12:14:17 +0000