aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2017-06-01[emacs] [toplevel] Make emacs flag local to the toplevel.Emilio Jesus Gallego Arias
We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel.
2017-06-01Merge PR#631: Fix bug #5255Maxime Dénès
2017-06-01Fix coq_makefile uninstall target under OSX.Maxime Dénès
2017-06-01Bump year in headers.Maxime Dénès
2017-06-01Merge PR#694: Fixing #5523 (missing support for complex constructions in ↵Maxime Dénès
recursive notations) (bis)
2017-06-01Fix bug #5019 (looping zify on dependent types)Jason Gross
This fixes [bug #5019](https://coq.inria.fr/bugs/show_bug.cgi?id=5019), "[zify] loops on dependent types"; before, we would see a `Z.of_nat (S ?k)` which could not be turned into `Z.succ (Z.of_nat k)`, add a hypothesis of the shape `0 <= Z.of_nat (S k)`, turn that into a hypothesis of the shape `0 <= Z.succ (Z.of_nat k)`, and loop forever on this. This may not be the "right" fix (there may be cases where `zify` should succeed where it still fails with this change), but this is a pure bugfix in the sense that the only places where it changes the behavior of `zify` are the places where, previously, `zify` looped forever.
2017-06-01Add opened bug 5019Jason Gross
2017-06-01Merge PR#710: Add test-suite checks for coqchk with constraintsMaxime Dénès
2017-06-01Merge PR#704: Fix empty parentheses display in test-suiteMaxime Dénès
2017-05-31Merge PR#701: [readlink -f] doesn't work on OSXMaxime Dénès
2017-05-31[travis] print failing test suite logs on failureGaëtan Gilbert
2017-05-31Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake ↵Maxime Dénès
(EDIT: for mutual fixpoints)
2017-05-31Tests for new specialize feature + CHANGES.Pierre Courtieu
2017-05-31Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with ↵Maxime Dénès
section variables.
2017-05-31Factorizing interp_gen through a function interpreting glob_constr.Hugo Herbelin
The new function is interp_glob_closure which is basically a renaming and generalization of interp_uconstr. Note a change of semantics that I could however not observe in practice. Formerly, interp_uconstr discarded ltac variables bound to names for interning, but interp_constr did not. Now, both discard them. We also export the new interp_glob_closure.
2017-05-31More precise on preventing clash between bound vars name and hidden impargs.Hugo Herbelin
We want to avoid capture in "Inductive I {A} := C : forall A, I". But in "Record I {A} := { C : forall A, A }.", non recursivity ensures that no clash will occur. This fixes previous commit, with which it could possibly be merged.
2017-05-31Fixing #5233 (missing implicit arguments for recursive records).Hugo Herbelin
Was failing e.g. with Inductive foo {A : Type} : Type := { Foo : foo }. Note: the test-suite was using the bug in coindprim.v.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 01:15:44 +0000