aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type "_som...Gravatar Maxime Dénès2017-10-06
|\
* \ Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an ...Gravatar Maxime Dénès2017-10-06
|\ \
* \ \ Merge PR #1124: Extraction: reduce atomic eta-redexes (solves indirectly BZ#4...Gravatar Maxime Dénès2017-10-06
|\ \ \
* \ \ \ Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 t...Gravatar Maxime Dénès2017-10-05
|\ \ \ \
* \ \ \ \ Merge PR #1107: Add coqwc tests to test suiteGravatar Maxime Dénès2017-10-05
|\ \ \ \ \
* \ \ \ \ \ Merge PR #1102: On the detection of evars which "advanced" (and a fix to BZ#5...Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #1101: Fixing an old proof engine bug in collecting evars with clear...Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \ \
| | | | | * | | Extraction: reduce eta-redexes whose cores are atomic (solves indirectly BZ#4...Gravatar Pierre Letouzey2017-10-05
| |_|_|_|/ / / |/| | | | | |
| | | | | | * Fixing BZ#5769 (variable of type "_something" was named after invalid "_").Gravatar Hugo Herbelin2017-10-05
| | | | | * | Fixing #5765 (an anomaly with 'pat in parameters of inductive definition).Gravatar Hugo Herbelin2017-10-05
| | | | | |/
* | | | | | Merge PR #1006: fix: ssrmatching and primitive projectionsGravatar Maxime Dénès2017-10-04
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #1078: Report missing arguments in error messageGravatar Maxime Dénès2017-10-04
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial).Gravatar Maxime Dénès2017-10-04
|\ \ \ \ \ \ \ \
| | | | | | * | | add coqwc testsGravatar Paul Steckler2017-10-03
| | | | | | | |/ | | | | | | |/|
* | | | | | | | Merge PR #1012: Make a test for coq_makefile portable.Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \
* | | | | | | | | [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
| |_|_|_|_|_|/ / |/| | | | | | |
| | | | | | * | Moving setting of "cleared" evar flag directly in Evd.restrict.Gravatar Hugo Herbelin2017-09-27
| | | | | | * | Fixing an old bug in collecting evars with cleared context.Gravatar Hugo Herbelin2017-09-27
| |_|_|_|_|/ / |/| | | | | |
| | | | | * | Fixing an old bug in collecting evars with cleared context.Gravatar Hugo Herbelin2017-09-27
| |_|_|_|/ / |/| | | | |
* | | | | | Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ...Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ...Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4...Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #1060: An optimization of tactic constructorGravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ \
| | | | * | | | | | | Fixing #5755 (discharging of inductive types not correct with let-ins).Gravatar Hugo Herbelin2017-09-23
| |_|_|/ / / / / / / |/| | | | | | | | |
| | * | | | | | | | Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).Gravatar Hugo Herbelin2017-09-23
| | | * | | | | | | Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Gravatar Hugo Herbelin2017-09-23
| |_|/ / / / / / / |/| | | | | | | |
| | | | * | | | | Make a test for coq_makefile portable.Gravatar Pierre-Marie Pédrot2017-09-22
| | | | | | * | | Report missing arguments in error messageGravatar Tej Chajed2017-09-21
| | | |_|_|/ / / | | |/| | | | |
* | / | | | | | A possible fix to BZ#5750 (ability to print context of ltac subterm match).Gravatar Hugo Herbelin2017-09-21
| |/ / / / / / |/| | | | | |
| | | | | * | ssr: fix canonical strucut key comparison with primproj onGravatar Enrico Tassi2017-09-20
| | | | |/ / | | | |/| |
| * | / | | An optimization of tactic constructor.Gravatar Hugo Herbelin2017-09-19
|/ / / / /
| | | * / Fixing bug #5741 (anomaly in info_trivial).Gravatar Hugo Herbelin2017-09-19
| |_|/ / |/| | |
* | | | Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).Gravatar Maxime Dénès2017-09-19
|\ \ \ \
| | * | | Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
| | * | | test-suite: polymorphismGravatar Matthieu Sozeau2017-09-19
| | * | | Allow declaring universe binders with no constraints with @{|}Gravatar Gaëtan Gilbert2017-09-19
| | * | | Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
| | |/ /
* | | | Merge PR #920: kernel: bugfix in filter_stack_domain.Gravatar Maxime Dénès2017-09-19
|\ \ \ \ | |_|/ / |/| | |
| * | | Add test-suite script by Cyprien ManginGravatar Matthieu Sozeau2017-09-18
* | | | Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" In...Gravatar Maxime Dénès2017-09-15
|\ \ \ \
* \ \ \ \ Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \
* \ \ \ \ \ Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match anon...Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \
| | | | | * | Avoid extra failure in the "constructor" tactic (bug #5666).Gravatar Guillaume Melquiond2017-09-14
| |_|_|_|/ / |/| | | | |
| | | | | * Adding a test for utf8 characters in directory names.Gravatar Hugo Herbelin2017-09-13
* | | | | | Fixing bug #5693 (treating empty notation format as any format).Gravatar Hugo Herbelin2017-09-12
* | | | | | Fixing a bug of recursive notations introduced in dfdaf4de.Gravatar Hugo Herbelin2017-09-12
* | | | | | Fixing little inaccuracy in coercions to ident or name.Gravatar Hugo Herbelin2017-09-12
| |_|_|_|/ |/| | | |
* | | | | Merge PR #1017: Addressing BZ#5713 (classical_left/classical_right artificial...Gravatar Maxime Dénès2017-09-11
|\ \ \ \ \
* \ \ \ \ \ Merge PR #997: coqdoc: Support comments in verbatim outputGravatar Maxime Dénès2017-09-07
|\ \ \ \ \ \