aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Collapse)AuthorAge
* Merge PR#633: An extension of EXTEND and notations to make standard parsing ↵Gravatar Maxime Dénès2017-05-17
|\ | | | | | | tricks available to users
* \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
|\ \
| | * Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.Gravatar Hugo Herbelin2017-05-16
| |/ |/|
| * Fixing a bug with nested "as" clauses in "match".Gravatar Hugo Herbelin2017-05-16
| |
* | Merge PR#594: An example showing the benefit of EconstrGravatar Maxime Dénès2017-05-11
|\ \
* \ \ Merge PR#201: Transparent abstractGravatar Maxime Dénès2017-05-11
|\ \ \
* \ \ \ Merge PR#558: Adding a fold_glob_constr_with_binders combinatorGravatar Maxime Dénès2017-05-05
|\ \ \ \
| | | * | Adding a test-suite pattern-unification example that Econstr fixed.Gravatar Hugo Herbelin2017-05-05
| |_|/ / |/| | |
* | | | Merge PR#544: Anonymous universesGravatar Maxime Dénès2017-05-05
|\ \ \ \
| * | | | Type@{_} should not produce a flexible algebraic universe.Gravatar Gaetan Gilbert2017-05-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Otherwise [(fun x => x) (Type : Type@{_})] becomes [(fun x : Type@{i+1} => x) (Type@{i} : Type@{i+1})] breaking the invariant that terms do not contain algebraic universes (at the lambda abstraction).
| * | | | Allow flexible anonymous universes in instances and sorts.Gravatar Gaetan Gilbert2017-05-03
| | | | | | | | | | | | | | | | | | | | The addition to the test suite showcases the usage.
* | | | | Merge PR#411: Mention template polymorphism in the documentation.Gravatar Maxime Dénès2017-05-03
|\ \ \ \ \ | |/ / / / |/| | | |
| | | | * Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions ↵Gravatar Maxime Dénès2017-05-02
| | | | |\ | | | | | | | | | | | | | | | | | | with evars).
| | | | * \ Merge PR#589: remove unneeded -emacs flag in coq-prog-args in test-suite filesGravatar Maxime Dénès2017-05-02
| | | | |\ \
| | | | * | | Fixing Set Rewriting Schemes bugs introduced in v8.5.Gravatar Hugo Herbelin2017-05-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Fixing a typo introduced in 31dbba5f. - Adapting to computation of universe constraints in pretyping. - Adding a regression test.
| | | | | * | remove unneeded -emacs flag to coq-prog-argsGravatar Paul Steckler2017-05-01
| | | | |/ /
| | | | | * Really fixing #2602 which was wrongly working because of #5487 hiding the cause.Gravatar Hugo Herbelin2017-05-01
| | | | |/ | | | | | | | | | | | | | | | | | | | | The cause was a missing evar/evar clause in ltac pattern-matching function (constr_matching.ml).
* | | | | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵Gravatar Maxime Dénès2017-04-28
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | let-ins
| | | | * | Add transparent_abstract tacticGravatar Jason Gross2017-04-25
| |_|_|/ / |/| | | |
* | | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\ \ \ \ \ | | |_|_|/ | |/| | |
| * | | | Fix anomaly when doing [all:Check _.] during a proof.Gravatar Gaetan Gilbert2017-04-14
| | | | |
| | | | * Using fold_glob_constr_with_binders to code bound_glob_vars.Gravatar Hugo Herbelin2017-04-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | To use the generic combinator, we introduce a side effect. I believe that we have more to gain from a short code than from being purely functional. This also fixes the expected semantics since the variables binding the return type in "match" were not taking into account.
| | | | * Adding a fold_glob_constr_with_binders combinator.Gravatar Hugo Herbelin2017-04-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Binding generalizable_vars_of_glob_constr, occur_glob_constr, free_glob_vars, and bound_glob_vars on it. Most of the functions of which it factorizes the code were bugged with respect to bindings in the return clause of "match" and in either the types or the bodies of "fix/cofix".
* | | | | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵Gravatar Maxime Dénès2017-04-12
|\ \ \ \ \ | |_|_|_|/ |/| | | | | | | | | record fields.
| | | | * Update various comments to use "template polymorphism"Gravatar Gaetan Gilbert2017-04-11
| |_|_|/ |/| | | | | | | | | | | Also remove obvious comments.
* | | | Merge PR#537: Efficient side-effect abstractionGravatar Maxime Dénès2017-04-11
|\ \ \ \
* | | | | Adding a test for 'rewrite in *' when an evar is solved by side-effect.Gravatar Pierre-Marie Pédrot2017-04-10
| | | | |
* | | | | Adding a test for the correctness of normalization in legacy typeclasses.Gravatar Pierre-Marie Pédrot2017-04-10
| | | | | | | | | | | | | | | | | | | | This is a test for commit 9d1230d484a2cf519f9cd76dc0f37815f3c6339b.
| | | | * Fixing several wrong computations of implicit arguments by positionGravatar Hugo Herbelin2017-04-09
| | | | | | | | | | | | | | | | | | | | in the presence of let-ins.
* | | | | Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\ \ \ \ \ | | |_|_|/ | |/| | |
| * | | | Merge PR#455: Farewell decl_modeGravatar Maxime Dénès2017-04-06
| |\ \ \ \
| | | | | * Merge branch 'origin/v8.5' into v8.6.Gravatar Hugo Herbelin2017-04-06
| | | | | |\ | | | | | | | | | | | | | | | | | | | | | Was needed to be done for a while.
| | | * | | | Adding tests for chained abstract tactics.Gravatar Pierre-Marie Pédrot2017-04-04
| | |/ / / / | |/| | | |
* | | | | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\| | | | |
| * | | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-03
| |\ \ \ \ \ | | | |_|/ / | | |/| | |
| | * | | | Instances should obey universe binders even when defined by tactics.Gravatar Gaetan Gilbert2017-04-03
| | | | | |
* | | | | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\| | | | |
| | | | * | Supporting arbitrary binders in record fields, including e.g. patterns.Gravatar Hugo Herbelin2017-03-23
| | |_|/ / | |/| | |
| * | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
| |\| | |
| | * | | Intern names bound in match patternsGravatar Tej Chajed2017-03-23
| | | | | | | | | | | | | | | | | | | | | | | | | Fixes Coq bug 5345 (https://coq.inria.fr/bugs/show_bug.cgi?id=5345): Cannot use names bound in matches inside Ltac definitions.
| * | | | Make IZR use a compact representation of integers.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | That way, (IZR 5) is no longer reduced to 2 + 1 + 1 + 1 (which is not convertible to 5) but instead to 1 + 2 * 2 (which is). Moreover, it means that, after reduction, real constants no longer exponentially blow up. Note that I was not able to fix the test-suite for the declarative mode, so the missing proof terms have been admitted.
| * | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-03-22
| |\| | |
| | | * | Farewell decl_modeGravatar Enrico Tassi2017-03-07
| | |/ / | |/| | | | | | | | | | | | | | This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests.
| | | * Fixing a little bug in using the "where" clause for inductive types.Gravatar Hugo Herbelin2017-02-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was not working when the inductive type had implicit parameters. This could still be improved. E.g. the following still does not work: Reserved Notation "#". Inductive I {A:Type} := C : # where "#" := I. But it should be made working by taking care of adding the mandatory implicit argument A at the time # is interpreted as [@I _] (i.e., technically speaking, using expl_impls in interp_notation).
| | * | reject notations that are both 'only printing' and 'only parsing'Gravatar Ralf Jung2017-02-16
| | | |
| | * | don't require printing-only notation to be productiveGravatar Ralf Jung2017-02-16
| | | |
* | | | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\ \ \ \
* | | | | Quick hack to fix interpretation of patterns in Ltac.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Interpretation of patterns in Ltac is essentially flawed. It does a roundtrip through the pretyper, and relies on suspicious flagging of evars in the evar source field to recognize original pattern holes. After the pattern_of_constr function was made evar-insensitive, it expanded evars that were solved by magical side-effects of the pretyper, even if it hadn't been asked to perform any heuristics. We backtrack on the insensitivity of the pattern_of_constr function. This may have a performance penalty in other dubious code, e.g. hints. In the long run we should get rid of the pattern_of_constr function.
| | * | | Add test-suite files for hintdb variables in Ltac.Gravatar Théo Zimmermann2017-02-07
| |/ / / | | | | | | | | | | | | In particular, this closes bug 2417.
| * | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
| |\| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 03:27:51 +0000