aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
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-17Fixing bug #5526,allow nonlinear variables in Notation patternsPaul Steckler
2017-05-17Merge PR#457: Adding an even more compact goal hyps mode.Maxime Dénès
2017-05-17fix swapping of ids in tuples, bug 5486Paul Steckler
2017-05-17Merge branch 'v8.6'Pierre-Marie Pédrot
2017-05-17Merge PR#620: Reorganization of the layout for miscellaneous testsMaxime Dénès
2017-05-16Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.Hugo Herbelin
2017-05-16Simplified compaction criterion + tests.Pierre Courtieu
2017-05-16Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters).Hugo Herbelin
We seized this opportunity to factorize the code for interning `pat with more general pre-existing code. More precisely: There was already a function to compute the free variables of a pattern. Commit c6d9d4fb rewrote an approximation of it and #5222 hits cases non-treated by this function. We remove the partially-defined redundant code and use instead the existing code since intern_cases_pattern, already called, was already doing this computation. (In doing so, we discover a bug in merging names in the presence of nested "as" clauses, which we fix in previous commit. Additionally, intern_local_pattern was misleadingly overkill to simply mean a folding on Id.Set.add and we avoid the detour.
2017-05-16Fixing a bug with nested "as" clauses in "match".Hugo Herbelin
2017-05-15Fix #5255: [Context (x : T := y)] should mean [Let x := y].Pierre-Marie Pédrot
2017-05-11Merge PR#594: An example showing the benefit of EconstrMaxime Dénès
2017-05-11Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 ↵Maxime Dénès
and 8.5/8.6 "refine"
2017-05-11Merge PR#201: Transparent abstractMaxime Dénès
2017-05-10Moving code for miscellaneous tests to specific files.Hugo Herbelin
The rule is that any file misc/*.sh will now be automatically executed from the test-file directory with appropriate environment variables set. The test can use any auxiliary material which is put in a directory of the same name as the test. This avoids making the main Makefile more or more complex. We loose some customization though (no more custom messages such as printing of the number of universes in the test about the number of necessary universes). We could preserve such customization if needed but I did not consider it was worth the effort. Warning: specific targets universes, deps-order, deps-checksum are removed by consistency. Do instead "make misc/universes.log", etc., or even "make misc" for all.
2017-05-10A more regular naming of variables in test-suite Makefile.Hugo Herbelin
2017-05-10Adding tests for testing exit status and #use"include".Hugo Herbelin
2017-05-10Cleaning old untested not any more interesting testing files.Hugo Herbelin
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-03FIx bug #5300: uncaught exception in "Print Assumptions".Cyprien Mangin
2017-05-03Merge PR#541: Fixing "decide equality" bug #5449Maxime 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-01Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Hugo Herbelin
The fix follows an invariant enforced in proofview.ml on the kind of evars that are goals or that occur in goals. One day, evar kinds will need a little cleaning... PS: This is a second attempt, completing db28e82 which was missing the case PEvar in constr_matching.ml. Indeed the attached fix to #5487 alone made #2602 failing, revealing that the real cause for #2602 was actually not fixed and that if the test for #2602 was working it was because of #5487 hiding the real problem in #2602.
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-30Fix bug #5501: Universe polymorphism breaks proof involving auto.Pierre-Marie Pédrot
A universe substitution was lacking as the normalized evar map was dropped.
2017-04-30Fixing "decide equality"'s bug #5449.Hugo Herbelin
The code was assuming that the terms t and u for which {t=u}+{t<>u} is proved were distinct. We refine an internal "generalize" of "u" so that it works on the two precise occurrences to abstract, even if other occurrences of u occur as subterm of t too. We also reuse the global constants found in the statement rather than reconstructing them (this seems better in case the global constants eventually get polymorphic universes?).
2017-04-28Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."Maxime Dénès
One day I'll get bored of spending my nights fixing commits that were pushed without being tested, and I'll ask for removal of push rights. But for now let's pretend I haven't insisted enough: ~~~~ PLEASE TEST YOUR COMMITS BEFORE PUSHING ~~~~ Thank you!
2017-04-28Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Hugo Herbelin
The fix follows an invariant enforced in proofview.ml on the kind of evars that are goals or that occur in goals. One day, evar kinds will need a little cleaning...
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-27Test for bug #5193: Uncaught exception Class_tactics.Search.ReachedLimitEx.Pierre-Marie Pédrot
2017-04-27Test surgical use of beta-iota in the type of variables coming fromHugo Herbelin
pattern-matching for refine.
2017-04-27Merge branch 'v8.6'Pierre-Marie Pédrot
2017-04-25Add transparent_abstract tacticJason Gross
2017-04-24Merge PR#574: Fix bug #5476: Ltac has an inconsistent view of hypotheses.Maxime Dénès
2017-04-24Merge PR#565: Remove VernacErrorMaxime Dénès
2017-04-22Merge branch v8.6 into trunkHugo Herbelin
Note: I removed what seemed to be dead code in recdef.ml (local_assum and local_def introduced with econstr branch), assuming that this is what should be done.
2017-04-21Remove VernacErrorGaetan Gilbert
2017-04-20Fix bug #5377: @? patterns broken.Pierre-Marie Pédrot
2017-04-19Fix bug #5476: Ltac has an inconsistent view of hypotheses.Pierre-Marie Pédrot
2017-04-19Merge PR#538: Correction of bug #4306Maxime Dénès
2017-04-17Add a test for bug #5321: clearbody breaks typing of goal.Pierre-Marie Pédrot
The bug has been solved as a side-effect of the EConstr branch.
2017-04-15Merge branch 'v8.6' into trunkMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 01:53:09 +0000