aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2017-05-31Fixing a failure to interpret some local implicit arguments in Inductive.Hugo Herbelin
For instance, the following was failing to use the implicitness of n: Inductive A (P:forall m {n}, n=m -> Prop) := C : P 0 eq_refl -> A P.
2017-05-31Fixing #5523 (missing support for complex constructions in recursive notations).Hugo Herbelin
We get rid of a complex function doing both an incremental comparison and an effect on names (Notation_ops.compare_glob_constr). For the effect on names, it was actually already done at the time of turning glob_constr to notation_constr, so it could be skipped here. For the comparison, we rely on a new incremental variant of Glob_ops.glob_eq_constr (thanks to Gaëtan for getting rid of the artificial recursivity in mk_glob_constr_eq). Seizing the opportunity to get rid of catch-all clauses in pattern-matching (as advocated by Maxime). Also make indentation closer to the one of other functions.
2017-05-31Fixing a too lax constraint for finding recursive binder part of a notation.Hugo Herbelin
This was preventing to work examples such as: Notation "[ x ; .. ; y ; z ]" := ((x,((fun u => u), .. (y,(fun u =>u,z)) ..))).
2017-05-30[gitlab] Artifact test suite logs on failure.Gaëtan Gilbert
2017-05-30Add test-suite checks for coqchk with constraintsJason Gross
2017-05-30Fix empty parentheses display in test-suiteJason Gross
There was an extra trailing space in #680. Now things display as, e.g., ``` TEST bugs/opened/3754.v TEST bugs/opened/4803.v (-compat 8.4) ``` instead of ``` TEST bugs/opened/3754.v ( ) TEST bugs/opened/4803.v (-compat 8.4 ) ```
2017-05-30Merge PR#693: A subtle bug in tclWITHHOLES.Maxime Dénès
2017-05-30[readlink -f] doesn't work on OSXGaëtan Gilbert
We only want an absolute path, no need to follow symlinks.
2017-05-30Support for using type information to infer more precise evar sources.Hugo Herbelin
This allows a better control on the name to give to an evar and, in particular, to address the issue about naming produced by "epose proof" in one of the comment of Zimmi48 at PR #248 (see file names.v). Incidentally updating output of Show output test (evar numbers shifted).
2017-05-30Few tests for e-variants of assert, set, remember.Hugo Herbelin
2017-05-30Fix bug 5550: "typeclasses eauto with" does not work with section variables.Théo Zimmermann
2017-05-29Merge PR#687: Gitlab CIMaxime Dénès
2017-05-29Omega: use "simpl" only on coefficents, not on atoms (fix #4132)Pierre Letouzey
Two issues in one: - some focused_simpl were called on the wrong locations - some focused_simpl were done on whole equations In the two cases, this could be bad if "simpl" goes too far with respect to what omega expects: later calls to "occurrence" might fail. This may happen for instance if an atom isn't a variable, but a let-in (b:=5:Z in the example).
2017-05-29Merge PR#546: Fix for bug #4499 and other minor related bugsMaxime Dénès
2017-05-28Merge PR#689: Changes to make coq-makefile not failing on MacOS X.Maxime Dénès
2017-05-28Fixing a subtle bug in tclWITHHOLES.Hugo Herbelin
This fixes Théo's bug on eset.
2017-05-28Merge PR#683: coq_makefile: build .cma for each .mlpackMaxime Dénès
2017-05-28Add equality lemmas for sig2 and sigT2Jason Gross
2017-05-28Add an [inversion_sigma] tacticJason Gross
This tactic does better than [inversion] at sigma types.
2017-05-28Merge PR#679: Bug 5546, qualify datatype constructors when needed in Show MatchMaxime Dénès
2017-05-28Merge PR#684: Trunk+fix coq makefile test suite on nixosMaxime Dénès
2017-05-28Gitlab CIGaëtan Gilbert
2017-05-28Merge PR#680: add Show test with -emacs flag for trunkMaxime Dénès
2017-05-27coq_makefile: build .cma for each .mlpackEnrico Tassi
It used to generate only .cmo (the packed one). While this works if the plugin has no external dependencies, it does not if it does. The bug affected only bytecode builds
2017-05-27Add execution permission to test-suite file.Théo Zimmermann
2017-05-27Use specific shell for more robustness.Théo Zimmermann
2017-05-27Fix test-suite/coq-makefile on NixOS.Théo Zimmermann
2017-05-26Changes to make coq-makefile not failing on MacOS X.Hugo Herbelin
There is still however a failure with "rmdir --ignore-fail-on-non-empty".
2017-05-26Merge PR#666: romega revisited : no more normalization trace, cleaned-up ↵Maxime Dénès
resolution trace
2017-05-26Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if ↵Maxime Dénès
printing only
2017-05-25add Show test with -emacs flagPaul Steckler
2017-05-25Bug 5546, qualify datatype constructors when neededPaul Steckler
2017-05-25Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsMaxime Dénès
2017-05-25Merge PR#406: coq makefile2Maxime Dénès
2017-05-24Merge PR#642: Small cleanup on `close_proof` type.Maxime Dénès
2017-05-24Merge PR#650: Fixing an extra bug with pattern_of_constrMaxime Dénès
2017-05-23add the only targetEnrico Tassi
This makes the following work correctly: make only TGTS="foo bar" -j2 note that make foo bar -j2 is not doing what you think
2017-05-23coq_makefile: don't quote extra arguments (-arg)Enrico Tassi
Restores compatibility with 8.6
2017-05-23test suite for coq_makefile2Enrico Tassi
2017-05-23test suite for coq_makefileEnrico Tassi
2017-05-23Merge PR#661: Added a test for #4765 (an example of printing abbreviation ↵Maxime Dénès
with binders)
2017-05-23Merge PR#657: [test-suite] Add tests for goal printing.Maxime Dénès
2017-05-23[vernac] Remove `Save.` command.Emilio Jesus Gallego Arias
It has been deprecated for a while in favor of `Qed`.
2017-05-22romega: discard constructor D_mono (shorter trace + fix a bug)Pierre Letouzey
For the bug, see new test test_romega10 in test-suite/success/ROmega0.v.
2017-05-22Using type classes in the interpretation of "specialize" and "contradiction".Hugo Herbelin
We do that by using constr_with_bindings rather than open_constr_with_bindings (+ extra call to typeclasses in "specialize"). If my understanding is right, the only effect would be to succeed more in cases where it was failing (in inh_conv_coerce_to_gen). In particular, "specialize" and "contradiction" already have a WITHHOLES test for rejecting pending holes. Incidentally, this answers enhancement #5153.
2017-05-20Added a test for #4765 (an example of printing abbreviation with binders).Hugo Herbelin
2017-05-20Merge PR#653: Bug #5535, test for Show with -emacsMaxime Dénès
2017-05-20Merge PR#474: A fix for #5390 (a useful error on used introduction names was ↵Maxime Dénès
masked).
2017-05-20[test-suite] Add tests for goal printing.Emilio Jesus Gallego Arias
- https://coq.inria.fr/bugs/show_bug.cgi?id=5529 - https://coq.inria.fr/bugs/show_bug.cgi?id=5537 See also PR #640
2017-05-19add test for Show with -emacs, bug 5535Paul Steckler
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-10 10:59:24 +0000