Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | | | * | | | | | add coqwc tests | Paul Steckler | 2017-10-03 | |
| | | | | | | |/ / / | | | | | | |/| | | | ||||
* | | | | | | | | | | Merge PR #1012: Make a test for coq_makefile portable. | Maxime Dénès | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ | ||||
* | | | | | | | | | | | [vernac] Remove `Qed exporting` syntax. | Emilio Jesus Gallego Arias | 2017-09-29 | |
| |_|_|_|_|_|/ / / / |/| | | | | | | | | | ||||
| | | | | | * | | | | Moving setting of "cleared" evar flag directly in Evd.restrict. | Hugo Herbelin | 2017-09-27 | |
| | | | | | * | | | | Fixing an old bug in collecting evars with cleared context. | Hugo Herbelin | 2017-09-27 | |
| |_|_|_|_|/ / / / |/| | | | | | | | | ||||
| | | | | * | | | | Fixing an old bug in collecting evars with cleared context. | Hugo Herbelin | 2017-09-27 | |
| |_|_|_|/ / / / |/| | | | | | | | ||||
* | | | | | | | | Merge PR #688: Binding universe constraints in Definition/Inductive/etc... | Maxime Dénès | 2017-09-26 | |
|\ \ \ \ \ \ \ \ | ||||
| | | | | | | * | | BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations | Paul Steckler | 2017-09-25 | |
* | | | | | | | | | Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ... | Maxime Dénès | 2017-09-25 | |
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ... | Maxime Dénès | 2017-09-25 | |
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4... | Maxime Dénès | 2017-09-25 | |
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1060: An optimization of tactic constructor | Maxime Dénès | 2017-09-25 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | * | | | | | | | | | Fixing #5755 (discharging of inductive types not correct with let-ins). | Hugo Herbelin | 2017-09-23 | |
| |_|_|/ / / / / / / / / |/| | | | | | | | | | | | ||||
| | * | | | | | | | | | | Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791). | Hugo Herbelin | 2017-09-23 | |
| | | |_|_|_|_|_|_|/ / | | |/| | | | | | | | | ||||
| | | * | | | | | | | | Fixing _rect bug for inductive types with let-ins and non-rec uniform params. | Hugo Herbelin | 2017-09-23 | |
| |_|/ / / / / / / / |/| | | | | | | | | | ||||
| | | | * | | | | | | Make a test for coq_makefile portable. | Pierre-Marie Pédrot | 2017-09-22 | |
| | | | | | * | | | | Report missing arguments in error message | Tej Chajed | 2017-09-21 | |
| | | |_|_|/ / / / | | |/| | | | | | | ||||
* | / | | | | | | | A possible fix to BZ#5750 (ability to print context of ltac subterm match). | Hugo Herbelin | 2017-09-21 | |
| |/ / / / / / / |/| | | | | | | | ||||
| | | | | * | | | ssr: fix canonical strucut key comparison with primproj on | Enrico Tassi | 2017-09-20 | |
| | | | |/ / / | | | |/| | | | ||||
| * | / | | | | An optimization of tactic constructor. | Hugo Herbelin | 2017-09-19 | |
|/ / / / / / | ||||
| | | * / / | Fixing bug #5741 (anomaly in info_trivial). | Hugo Herbelin | 2017-09-19 | |
| |_|/ / / |/| | | | | ||||
* | | | | | Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666). | Maxime Dénès | 2017-09-19 | |
|\ \ \ \ \ | ||||
| | * | | | | Don't lose names in UState.universe_context. | Gaëtan Gilbert | 2017-09-19 | |
| | * | | | | test-suite: polymorphism | Matthieu Sozeau | 2017-09-19 | |
| | * | | | | Allow declaring universe binders with no constraints with @{|} | Gaëtan Gilbert | 2017-09-19 | |
| | * | | | | Allow declaring universe constraints at definition level. | Matthieu Sozeau | 2017-09-19 | |
| | |/ / / | ||||
* | | | | | Merge PR #920: kernel: bugfix in filter_stack_domain. | Maxime Dénès | 2017-09-19 | |
|\ \ \ \ \ | |_|/ / / |/| | | | | ||||
| * | | | | Add test-suite script by Cyprien Mangin | Matthieu Sozeau | 2017-09-18 | |
* | | | | | Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" In... | Maxime Dénès | 2017-09-15 | |
|\ \ \ \ \ | ||||
* \ \ \ \ \ | Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work... | Maxime Dénès | 2017-09-15 | |
|\ \ \ \ \ \ | ||||
* \ \ \ \ \ \ | Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match anon... | Maxime Dénès | 2017-09-15 | |
|\ \ \ \ \ \ \ | ||||
| | | | | * | | | Avoid extra failure in the "constructor" tactic (bug #5666). | Guillaume Melquiond | 2017-09-14 | |
| |_|_|_|/ / / |/| | | | | | | ||||
| | | | | * | | Adding a test for utf8 characters in directory names. | Hugo Herbelin | 2017-09-13 | |
* | | | | | | | Fixing bug #5693 (treating empty notation format as any format). | Hugo Herbelin | 2017-09-12 | |
* | | | | | | | Fixing a bug of recursive notations introduced in dfdaf4de. | Hugo Herbelin | 2017-09-12 | |
* | | | | | | | Fixing little inaccuracy in coercions to ident or name. | Hugo Herbelin | 2017-09-12 | |
| |_|_|_|/ / |/| | | | | | ||||
* | | | | | | Merge PR #1017: Addressing BZ#5713 (classical_left/classical_right artificial... | Maxime Dénès | 2017-09-11 | |
|\ \ \ \ \ \ | ||||
* \ \ \ \ \ \ | Merge PR #997: coqdoc: Support comments in verbatim output | Maxime Dénès | 2017-09-07 | |
|\ \ \ \ \ \ \ | ||||
* | | | | | | | | fix test-suite/coq-makefile/findlib-package on windows | Enrico Tassi | 2017-09-04 | |
| | * | | | | | | Addressing BZ#5713 (classical_left/classical_right artificially restricted). | Hugo Herbelin | 2017-09-03 | |
| |/ / / / / / |/| | | | | | | ||||
* | | | | | | | Merge PR #996: Fix BZ#5697: Congruence does not work with primitive projections | Maxime Dénès | 2017-08-31 | |
|\ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ | Merge PR #995: Program: fix BZ#5683, missing lift when building case predicate | Maxime Dénès | 2017-08-31 | |
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flag | Maxime Dénès | 2017-08-31 | |
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR #958: coq_makefile: build/use .cma for packed plugins too | Maxime Dénès | 2017-08-31 | |
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #998: Avoid running interactive tests on Windows. | Maxime Dénès | 2017-08-30 | |
|\ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | * | | | Fixing part of #5707 (allowing destruct to use non dependent case analysis). | Hugo Herbelin | 2017-08-30 | |
| | * | | | | | | | | | | coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxs | Enrico Tassi | 2017-08-29 | |
| * | | | | | | | | | | | Avoid running interactive tests on Windows. | Maxime Dénès | 2017-08-29 | |
| | | | | * | | | | | | | Properly handling parameters of primitive projections in cctac. | Pierre-Marie Pédrot | 2017-08-29 | |
| | | | | * | | | | | | | Fix BZ#5697: Congruence does not work with primitive projections. | Pierre-Marie Pédrot | 2017-08-29 | |
| |_|_|_|/ / / / / / / |/| | | | | | | | | | |