aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2015-12-02Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Hugo Herbelin
2015-11-30Test for bug #4149.Pierre-Marie Pédrot
2015-11-28Test-suite files for closed bugsMatthieu Sozeau
2015-11-28Closed bugs.Matthieu Sozeau
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
2015-11-26Fixing the "parsing rules with idents later declared as keywords" problem.Hugo Herbelin
2015-11-22Fixing a vm_compute bug in the presence of let-ins among theHugo Herbelin
2015-11-22Fixing a bug of adjust_subst_to_rel_context.Hugo Herbelin
2015-11-22Fixing kernel bug in typing match with let-ins in the arity.Hugo Herbelin
2015-11-19Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.Pierre-Marie Pédrot
2015-11-18Fixing logical bugs in the presence of let-ins in computiong primitiveHugo Herbelin
2015-11-12Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.Pierre-Marie Pédrot
2015-11-12Fixed test-suite file for bug #3998.Matthieu Sozeau
2015-11-11Now closed.Matthieu Sozeau
2015-11-11Fix bug #3257, setoid_reflexivity should fail if not completing the goal.Matthieu Sozeau
2015-11-11Fix bug #4293: ensure let-ins do not contain algebraic universes inMatthieu Sozeau
2015-11-11Fixing bug #3554: Anomaly: Anonymous implicit argument.Pierre-Marie Pédrot
2015-11-10Test for bug #4404.Pierre-Marie Pédrot
2015-11-07Fixing output test Existentials.v after eec77191b.Hugo Herbelin
2015-11-07Tests for syntax "Show id" and [id]:tac (shelved or not).Hugo Herbelin
2015-11-06Fixing complexity file f_equal.v.Hugo Herbelin
2015-11-06Fixing complexity issue with f_equal. Thanks to J.-H. JourdanHugo Herbelin
2015-11-05Add test-suite file for #4273.Matthieu Sozeau
2015-11-04Univs: missing checks in evarsolve with candidates and missing aMatthieu Sozeau
2015-11-04Hint Cut documentation and cleanup of printing (was duplicated andMatthieu Sozeau
2015-11-04Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusionMatthieu Sozeau
2015-11-04Test file for #4397.Maxime Dénès
2015-11-02Fix bug #4151: discrepancy between exact and eexact/eassumption.Matthieu Sozeau
2015-11-02Refresh rigid universes as well, and in 8.4 compatibility mode,Matthieu Sozeau
2015-10-29Handle side-effects of Vernacular commands inside proofs better, so thatMatthieu Sozeau
2015-10-29Fixing another instance of bug #3267 in eauto, this time in theHugo Herbelin
2015-10-28Fix test suite after Matthieu's ed7af646f2e486b.Maxime Dénès
2015-10-28test cases.Gregory Malecha
2015-10-28Univs: fix bug #4375, accept universe binders on (co)-fixpointsMatthieu Sozeau
2015-10-28Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins"Hugo Herbelin
2015-10-27Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesMatthieu Sozeau
2015-10-26Two test-suite files for bugs 3974 and 3975Pierre Letouzey
2015-10-24Backtracking on interpreting toplevel calls to exact in scope determinedHugo Herbelin
2015-10-22Fixing a bug in reporting ill-formed inductive.Hugo Herbelin
2015-10-21Bug #3956 is fixed.Matthieu Sozeau
2015-10-19Test for #4372 (anomaly in inversion in the presence of fake dependency).Hugo Herbelin
2015-10-18Fixing #4198 (continued): not matching within the inner lambdas/let-insHugo Herbelin
2015-10-17Test for bug #4325.Pierre-Marie Pédrot
2015-10-15Test file for #4346: Set is no longer of type TypeMaxime Dénès
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-11Adding test for bug #4366.Pierre-Marie Pédrot
2015-10-11Fixing test-suiteHugo Herbelin
2015-10-11Fixing untimely unexpected warning "Collision between bound variables" (#4317).Hugo Herbelin
2015-10-11Refining 0c320e79ba30 in fixing interpretation of constr under bindersHugo Herbelin
2015-10-09Refine fix for handling of the universe contexts of hints, depending onMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 14:52:02 +0000