aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Collapse)Author
2017-06-06Merge PR#600: Some factorizations of ltac interpretation functions between ↵Maxime Dénès
ssreflect and coq code
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
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 ```
2017-06-01Merge PR#449: make specialize smarter (bug 5370).Maxime Dénès
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-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-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-28Fixing a subtle bug in tclWITHHOLES.Hugo Herbelin
This fixes Théo's bug on eset.
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-26Merge PR#666: romega revisited : no more normalization trace, cleaned-up ↵Maxime Dénès
resolution trace
2017-05-25Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsMaxime Dénès
2017-05-24Merge PR#642: Small cleanup on `close_proof` type.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-19Fixing an extra bug with pattern_of_constr.Hugo Herbelin
Ensure in type constr_pattern that those preexisting existential variables of the goal which do not contribute as pattern variables are expanded: constr_pattern is not observed up to evar expansion (like EConstr does), so we need to pre-normalize defined evars in patterns to that matching against an EConstr works.
2017-05-17Merge PR#633: An extension of EXTEND and notations to make standard parsing ↵Maxime Dénès
tricks available to users
2017-05-17Merge branch 'v8.6'Pierre-Marie Pédrot
2017-05-16Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.Hugo Herbelin
2017-05-16Fixing a bug with nested "as" clauses in "match".Hugo Herbelin
2017-05-11Merge PR#594: An example showing the benefit of EconstrMaxime Dénès
2017-05-11Merge PR#201: Transparent abstractMaxime Dénès
2017-05-05Merge PR#558: Adding a fold_glob_constr_with_binders combinatorMaxime Dénès
2017-05-05Adding a test-suite pattern-unification example that Econstr fixed.Hugo Herbelin
2017-05-05Merge PR#544: Anonymous universesMaxime Dénès
2017-05-03Type@{_} should not produce a flexible algebraic universe.Gaetan Gilbert
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).
2017-05-03Allow flexible anonymous universes in instances and sorts.Gaetan Gilbert
The addition to the test suite showcases the usage.
2017-05-03Merge PR#411: Mention template polymorphism in the documentation.Maxime Dénès
2017-05-02Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions ↵Maxime Dénès
with evars).
2017-05-02Merge PR#589: remove unneeded -emacs flag in coq-prog-args in test-suite filesMaxime Dénès
2017-05-01Fixing Set Rewriting Schemes bugs introduced in v8.5.Hugo Herbelin
- Fixing a typo introduced in 31dbba5f. - Adapting to computation of universe constraints in pretyping. - Adding a regression test.
2017-05-01remove unneeded -emacs flag to coq-prog-argsPaul Steckler
2017-05-01Really fixing #2602 which was wrongly working because of #5487 hiding the cause.Hugo Herbelin
The cause was a missing evar/evar clause in ltac pattern-matching function (constr_matching.ml).
2017-04-28Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵Maxime Dénès
let-ins
2017-04-25Add transparent_abstract tacticJason Gross
2017-04-15Merge branch 'v8.6' into trunkMaxime Dénès
2017-04-14Fix anomaly when doing [all:Check _.] during a proof.Gaetan Gilbert
2017-04-13Reinstate fixpoint refolding in [cbn], deactivated by mistake.Matthieu Sozeau
Add a test-suite file to be sure we won't regress silently.
2017-04-13Using fold_glob_constr_with_binders to code bound_glob_vars.Hugo Herbelin
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.
2017-04-13Adding a fold_glob_constr_with_binders combinator.Hugo Herbelin
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".
2017-04-12Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵Maxime Dénès
record fields.
2017-04-11Update various comments to use "template polymorphism"Gaetan Gilbert
Also remove obvious comments.
2017-04-11Merge PR#537: Efficient side-effect abstractionMaxime Dénès
2017-04-10Adding a test for 'rewrite in *' when an evar is solved by side-effect.Pierre-Marie Pédrot
2017-04-10Adding a test for the correctness of normalization in legacy typeclasses.Pierre-Marie Pédrot
This is a test for commit 9d1230d484a2cf519f9cd76dc0f37815f3c6339b.
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-07 11:11:51 +0000