aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* Correct some spelling errorsmasterGravatar Benjamin Barenblat2018-07-22
| | | | | | | | | | Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`.
* Merge PR #7941: Extend QuestionMark to produce a better error message in ↵Gravatar Pierre-Marie Pédrot2018-07-19
|\ | | | | | | case of missing record field
* \ Merge PR #8054: [dev] Autogenerate OCaml dev files.Gravatar Enrico Tassi2018-07-18
|\ \
* | | Remove fourier pluginGravatar Maxime Dénès2018-07-17
| | | | | | | | | | | | As stated in the manual, the fourier tactic is subsumed by lra.
| | * Change QuestionMark for better record field missing error message.Gravatar Siddharth Bhat2018-07-17
| |/ |/| | | | | | | | | | | | | | | | | While we were adding a new field into `QuestionMark`, we decided to go ahead and refactor the constructor to hold an actual record. This record now holds the name, obligations, and whether the evar represents a missing record field. This is used to provide better error messages on missing record fields.
| * [dev] Autogenerate OCaml dev files.Gravatar Emilio Jesus Gallego Arias2018-07-12
| | | | | | | | | | | | | | | | For now we only copy the templates, but we could do more fancy stuff. This helps to be compatible with build systems that take care of these files automatically, see: https://github.com/coq/coq/pull/6857#discussion_r202096579
* | Tactic deprecation machineryGravatar Maxime Dénès2018-07-12
|/ | | | | | | | | | | | | | | | | | | | | | | | | | | We make it possible to deprecate tactics defined by `Ltac`, `Tactic Notation` or ML. For the first two variants, we anticipate the syntax of attributes: `#[deprecated(since = "XX", note = "YY")]` In ML, the syntax is: ``` let reflexivity_depr = let open CWarnings in { since = "8.5"; note = "Use admit instead." } TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] END ``` A warning is shown at the point where the tactic is used (either a direct call or when defining another tactic): Tactic `foo` is deprecated since XX. YY YY is typically meant to be "Use bar instead.".
* Merge PR #7920: Generic syntax for attributesGravatar Maxime Dénès2018-07-09
|\
* \ Merge PR #7884: Fix #5719: Uncaught exception Invalid_argument.Gravatar Matthieu Sozeau2018-07-09
|\ \
* | | Add test for #8004.Gravatar Gaëtan Gilbert2018-07-06
| | |
* | | Convert timing tools to run with both python2 and python3Gravatar Jasper Hugunin2018-07-04
| | |
| | * [test suite] Test case for attributesGravatar Vincent Laporte2018-07-03
| |/ |/|
* | Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsGravatar Pierre-Marie Pédrot2018-07-03
|\ \
| * | hints: add Hint Variables/Constants Opaque/Transparent commandsGravatar Matthieu Sozeau2018-07-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables
* | | Add test for Uniform Inductive ParametersGravatar Jasper Hugunin2018-07-01
|/ /
* | Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation ↵Gravatar Emilio Jesus Gallego Arias2018-07-01
|\ \ | | | | | | | | | format).
* | | Workaround to fix #7731 (printing not splitting line at break hint).Gravatar Hugo Herbelin2018-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In some cases, Format's inner boxes inside an outer box act as break hints, even though there are already "better" break hints in the outer box. We work around this "feature" by not inserting a box around the default printing rule for a notation if there is no effective break points in the box. See https://caml.inria.fr/mantis/view.php?id=7804 for the related OCaml discussion.
| * | Fixes #7712 (an anomaly in reporting bad recursive notation format).Gravatar Hugo Herbelin2018-06-29
|/ /
* | Merge PR #7860: Fix #7704: Launching coqide through PATH fails.Gravatar Emilio Jesus Gallego Arias2018-06-28
|\ \
* \ \ Merge PR #7866: Implementation of mutual records in the higher strataGravatar Maxime Dénès2018-06-28
|\ \ \
* \ \ \ Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)Gravatar Pierre-Marie Pédrot2018-06-27
|\ \ \ \
| * | | | Test file for #7723Gravatar Maxime Dénès2018-06-27
| | | | |
* | | | | Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).Gravatar Hugo Herbelin2018-06-26
|/ / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We fix the issue by removing terms of the substitutions which have free variables and are thus not interpretable in the context of the "ltac:" subterm. This remains rather ad hoc, since, in an expression "Notation f x := ltac:(foo)", we interpret "x" at calling time of "foo" rather than at use time of "x" in foo, even if "x" is not necessary. We could also imagine that binders in the ltac expressions are then interpreted but that would start to be (very) complicated. Note that this will presumably "fix" ltac2 quotations at the same time.
* | | | Merge PR #7798: Remove hack skipping comparison of algebraic universes in ↵Gravatar Matthieu Sozeau2018-06-25
|\ \ \ \ | | | | | | | | | | | | | | | subtyping.
* \ \ \ \ Merge PR #7559: Existing Class noop when already a class + warning.Gravatar Matthieu Sozeau2018-06-25
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7620: [ssr] rewrite: turn anomaly into regular errorGravatar Maxime Dénès2018-06-25
|\ \ \ \ \ \
| | | | * | | Adding various tests for mutual records.Gravatar Pierre-Marie Pédrot2018-06-24
| |_|_|/ / / |/| | | | |
* | | | | | Merge PR #7236: [ssr] simpler semantics for delayed clearsGravatar Maxime Dénès2018-06-23
|\ \ \ \ \ \
| | | | | * | Fix #7704: get_toplevel_path needs normalised argv.(0)Gravatar Gaëtan Gilbert2018-06-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When launched through PATH argv.(0) is just the command name. eg "coqtop -compile foo.v" -> argv.(0) = "coqtop" Using executable_name also follows symlinks but this isn't tested to avoid messing with windows. Running Coq through a symlink is not as important as PATH anyways.
| | | | * | | Remove hack skipping comparison of algebraic universes in subtyping.Gravatar Gaëtan Gilbert2018-06-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When inferring [u <= v+k] I replaced the exception and instead add [u <= v]. This is trivially sound and it doesn't seem possible to have the one without the other (except specially for [Set <= v+k] which was already handled). I don't know an example where this used to fail and now succeeds (the point was to remove an anomaly, but the example ~~~ Module Type SG. Definition DG := Type. End SG. Module MG : SG. Definition DG := Type : Type. Fail End MG. ~~~ now fails with universe inconsistency. Fix #7695 (soundness bug!).
| * | | | | | [ssr] implement {}/v as a short hand for {v}/v when v is an idGravatar Enrico Tassi2018-06-22
| | |_|/ / / | |/| | | |
* / | | | | [ssr] test case for rewrite and set on univ poly keysGravatar Enrico Tassi2018-06-22
|/ / / / /
| | | | * Fix #5719: Uncaught exception Invalid_argument.Gravatar Pierre-Marie Pédrot2018-06-21
| |_|_|/ |/| | | | | | | | | | | | | | | | | | | It seems that lifting a term with a negative index is not equivalent to strengthening it by applying to a dummy substitution. This looks suspicious at best.
| * | | [ssr] test case for rewrite (setoid) making the goal illtypedGravatar Enrico Tassi2018-06-20
|/ / /
* | | Merge PR #6754: Better elaboration of pattern-matchings on primitive projectionsGravatar Pierre-Marie Pédrot2018-06-19
|\ \ \
* | | | Fix #7421: constr_eq ignores universe constraints.Gravatar Gaëtan Gilbert2018-06-18
| |_|/ |/| | | | | | | | | | | The test isn't quite the one in #7421 because that use of algebraic universes is wrong.
* | | Merge PR #7824: Fixes #7811 (uncaught Not_found in notation printer related ↵Gravatar Pierre-Marie Pédrot2018-06-17
|\ \ \ | | | | | | | | | | | | to "match").
* \ \ \ Merge PR #7818: Do not allow spliting in res_pf, this is reserved for pretypingGravatar Pierre-Marie Pédrot2018-06-17
|\ \ \ \
| | * | | Fixes #7811 (uncaught Not_found in notation printer related to "match").Gravatar Hugo Herbelin2018-06-17
| |/ / / |/| | |
* | | | Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.Gravatar Maxime Dénès2018-06-17
|\ \ \ \
| | | * | Add test-suite case for performance, had to use TimeoutGravatar Matthieu Sozeau2018-06-15
| | | | |
| | | * | Better elaboration of pattern-matchings on primitive projectionsGravatar Matthieu Sozeau2018-06-15
| |_|/ / |/| | | | | | | | | | | | | | | This ensures that computations are shared as much as possible, mimicking the "positive" records computational behavior if possible.
| | * | Do not allow spliting in res_pf, this is reserved for pretypingGravatar Matthieu Sozeau2018-06-15
| | | |
* | | | Workaround to handle non-value arguments in tactics.Gravatar Cyprien Mangin2018-06-14
| |/ / |/| | | | | | | | | | | Although the fix is not a proper one, it seems to solve every instance of #2800 that could be tested.
* | | Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ↵Gravatar Pierre-Marie Pédrot2018-06-14
|\ \ \ | | | | | | | | | | | | of submodules.
* \ \ \ Merge PR #664: Fixing #5500 (missing test in return clause of match leading ↵Gravatar Matthieu Sozeau2018-06-14
|\ \ \ \ | | | | | | | | | | | | | | | to anomaly)
* \ \ \ \ Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder ↵Gravatar Matthieu Sozeau2018-06-14
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | in unification
* \ \ \ \ \ Merge PR #7771: Tweak printing boxes for unicode bindersGravatar Hugo Herbelin2018-06-14
|\ \ \ \ \ \
* | | | | | | Markdown docs: switch from absolute to relative links.Gravatar Théo Zimmermann2018-06-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We had mostly used absolute links in the past. I just discovered that GitHub recommends using relative links instead: https://help.github.com/articles/basic-writing-and-formatting-syntax/#relative-links and indeed my Emacs Markdown mode can handle relative links but doesn't interpret absolute links relatively to the root of the git repository. [ci skip]
* | | | | | | Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").Gravatar Hugo Herbelin2018-06-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a quick fix. Code should be made nicer along these lines: - try to pass the name of the variable created by "mkletin_goal" in the monad using "refine_one"; - use a disjunctive type of "inhyps" to indicate when it is meaningful, rather than using [].
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 14:14:15 +0000