aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* Merge PR#709: Bytecode compilation apart from 'make world', againGravatar Maxime Dénès2017-06-12
|\
* | Add support for "-bypass-API" argument of "coq_makefile"Gravatar Matej Košík2017-06-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Plugin-writers can now use: -bypass-API parameter with "coq_makefile". The effect of that is that instead of -I API the plugin will be compiled with: -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
* | make test-suite/save-logs.sh usable also on old MacOS XGravatar Maxime Denes2017-06-12
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \
* \ \ Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a ↵Gravatar Maxime Dénès2017-06-06
|\ \ \ | | | | | | | | | | | | short econstr-cleaning of record.ml
* \ \ \ Merge PR#600: Some factorizations of ltac interpretation functions between ↵Gravatar Maxime Dénès2017-06-06
|\ \ \ \ | | | | | | | | | | | | | | | ssreflect and coq code
* | | | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
* | | | | Merge PR#691: [travis] Add OSX test-suite checking.Gravatar Maxime Dénès2017-06-02
|\ \ \ \ \
| | | | * \ Merge PR#705: Fix bug #5019 (looping zify on dependent types)Gravatar Maxime Dénès2017-06-02
| | | | |\ \
* | | | | \ \ Merge PR#647: [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Maxime Dénès2017-06-02
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR#711: [gitlab] Artifact test suite logs on failure.Gravatar Maxime Dénès2017-06-02
|\ \ \ \ \ \ \ \
| | | * | | | | | Test-suite: do not test native compiler if disabled by configure.Gravatar Maxime Dénès2017-06-01
| | | | | | | | |
| | | | | | | | * test-suite/coq-makefile: we do not build byte file by default anymoreGravatar Pierre Letouzey2017-06-01
| | | | | | | | |
* | | | | | | | | Merge PR#449: make specialize smarter (bug 5370).Gravatar Maxime Dénès2017-06-01
|\ \ \ \ \ \ \ \ \
| | | * | | | | | | [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-06-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel.
| | | | | | | * | | Merge PR#631: Fix bug #5255Gravatar Maxime Dénès2017-06-01
| | | | | | | |\ \ \
| | | | * | | | | | | Fix coq_makefile uninstall target under OSX.Gravatar Maxime Dénès2017-06-01
| | | |/ / / / / / /
* | | | | | | | | | Merge PR#694: Fixing #5523 (missing support for complex constructions in ↵Gravatar Maxime Dénès2017-06-01
|\ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | recursive notations) (bis)
| | | | | | | | * | Fix bug #5019 (looping zify on dependent types)Gravatar Jason Gross2017-06-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | | * | Add opened bug 5019Gravatar Jason Gross2017-06-01
| | | | | | | | | |
| | | | | | * | | | Merge PR#710: Add test-suite checks for coqchk with constraintsGravatar Maxime Dénès2017-06-01
| | | | | | |\ \ \ \ | | | | | | | |_|/ / | | | | | | |/| | |
* | | | | | | | | | Merge PR#704: Fix empty parentheses display in test-suiteGravatar Maxime Dénès2017-06-01
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR#701: [readlink -f] doesn't work on OSXGravatar Maxime Dénès2017-05-31
|\ \ \ \ \ \ \ \ \ \ \
| | | | | * | | | | | | [travis] print failing test suite logs on failureGravatar Gaëtan Gilbert2017-05-31
| | | | | | | | | | | |
| | | | | | | | * | | | Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake ↵Gravatar Maxime Dénès2017-05-31
| | | | | | | | |\ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (EDIT: for mutual fixpoints)
| | | | * | | | | | | | | Tests for new specialize feature + CHANGES.Gravatar Pierre Courtieu2017-05-31
| | | | | |_|_|_|_|_|_|/ | | | | |/| | | | | | |
| | | | | | | | * | | | Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with ↵Gravatar Maxime Dénès2017-05-31
| | | | | | | | |\ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | section variables.
| | | | | | * | | | | | | Factorizing interp_gen through a function interpreting glob_constr.Gravatar Hugo Herbelin2017-05-31
| | | | | |/ / / / / / / | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | * | | | | | More precise on preventing clash between bound vars name and hidden impargs.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | * | | | | | Fixing #5233 (missing implicit arguments for recursive records).Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was failing e.g. with Inductive foo {A : Type} : Type := { Foo : foo }. Note: the test-suite was using the bug in coindprim.v.
| | | | | | * | | | | | Fixing a failure to interpret some local implicit arguments in Inductive.Gravatar Hugo Herbelin2017-05-31
| | | | | |/ / / / / / | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | * | | | | | | | Fixing #5523 (missing support for complex constructions in recursive notations).Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | * | | | | | | | Fixing a too lax constraint for finding recursive binder part of a notation.Gravatar Hugo Herbelin2017-05-31
| | | |/ / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was preventing to work examples such as: Notation "[ x ; .. ; y ; z ]" := ((x,((fun u => u), .. (y,(fun u =>u,z)) ..))).
| | | | * / / / / / [gitlab] Artifact test suite logs on failure.Gravatar Gaëtan Gilbert2017-05-30
| | | |/ / / / / /
| | | | | | | * / Add test-suite checks for coqchk with constraintsGravatar Jason Gross2017-05-30
| | | | | |_|/ / | | | | |/| | |
| | * | / | | | Fix empty parentheses display in test-suiteGravatar Jason Gross2017-05-30
| | |/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 ) ```
| | | * | | | Merge PR#693: A subtle bug in tclWITHHOLES.Gravatar Maxime Dénès2017-05-30
| | | |\ \ \ \
| * | | | | | | [readlink -f] doesn't work on OSXGravatar Gaëtan Gilbert2017-05-30
| |/ / / / / / | | | | | | | | | | | | | | | | | | | | | We only want an absolute path, no need to follow symlinks.
* | | | | | | Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
* | | | | | | Few tests for e-variants of assert, set, remember.Gravatar Hugo Herbelin2017-05-30
|/ / / / / /
| | | * | | Fix bug 5550: "typeclasses eauto with" does not work with section variables.Gravatar Théo Zimmermann2017-05-30
| | | | | |
* | | | | | Merge PR#687: Gitlab CIGravatar Maxime Dénès2017-05-29
|\ \ \ \ \ \
| | * | | | | Omega: use "simpl" only on coefficents, not on atoms (fix #4132)Gravatar Pierre Letouzey2017-05-29
| | | |/ / / | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
| | * | | | Merge PR#546: Fix for bug #4499 and other minor related bugsGravatar Maxime Dénès2017-05-29
| | |\ \ \ \
* | | \ \ \ \ Merge PR#689: Changes to make coq-makefile not failing on MacOS X.Gravatar Maxime Dénès2017-05-28
|\ \ \ \ \ \ \
| | | | | * | | Fixing a subtle bug in tclWITHHOLES.Gravatar Hugo Herbelin2017-05-28
| | | | |/ / / | | | |/| | | | | | | | | | | | | | | | | This fixes Théo's bug on eset.
* | | | | | | Merge PR#683: coq_makefile: build .cma for each .mlpackGravatar Maxime Dénès2017-05-28
|\ \ \ \ \ \ \
| | | | * \ \ \ Merge PR#679: Bug 5546, qualify datatype constructors when needed in Show MatchGravatar Maxime Dénès2017-05-28
| | | | |\ \ \ \
* | | | | \ \ \ \ Merge PR#684: Trunk+fix coq makefile test suite on nixosGravatar Maxime Dénès2017-05-28
|\ \ \ \ \ \ \ \ \
| | | | * | | | | | Gitlab CIGravatar Gaëtan Gilbert2017-05-28
| | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-21 16:42:02 +0000