aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Fix bug #4480: progress was not checked for setoid_rewrite.Gravatar Matthieu Sozeau2016-01-07
* Put implicits back as in 8.4.Gravatar Matthieu Sozeau2015-12-31
* Fix bug #4456, anomaly in handle-side effectsGravatar Matthieu Sozeau2015-12-31
* Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found.Gravatar Pierre-Marie Pédrot2015-12-29
* Inclusion of functors with restricted signature is now forbidden (fix #3746)Gravatar Pierre Letouzey2015-12-22
* (Partial) fix for bug #4453: raise an error instead of an anomaly.Gravatar Matthieu Sozeau2015-12-17
* Proof using: do not clear unused section hyps automaticallyGravatar Enrico Tassi2015-12-15
* Fix test suite after change in extraction.Gravatar Maxime Dénès2015-12-15
* Extraction: more cautious use of intermediate result caching (fix #3923)Gravatar Pierre Letouzey2015-12-15
* Fix test-suite files after change in refine tactic.Gravatar Maxime Dénès2015-12-15
* Adding a test for the unshelve tactical.Gravatar Pierre-Marie Pédrot2015-12-15
* Refine tactic now shelves unifiable holes.Gravatar Pierre-Marie Pédrot2015-12-15
* extraction_impl.v: fix a typoGravatar Pierre Letouzey2015-12-14
* A test file for Extraction Implicit (including bugs #4243 and #4228)Gravatar Pierre Letouzey2015-12-14
* Test file for #4363 was not complete.Gravatar Maxime Dénès2015-12-14
* Univs: Fix bug #4363, nested abstract.Gravatar Matthieu Sozeau2015-12-11
* Fixing a pat%constr bug. Thanks to Enrico for reporting.Gravatar Hugo Herbelin2015-12-10
* Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Gravatar Hugo Herbelin2015-12-10
* bug fixes to vm computation + test cases.Gravatar Gregory Malecha2015-12-09
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Gravatar Hugo Herbelin2015-12-05
* Univs: fix bug #4443.Gravatar Matthieu Sozeau2015-12-03
* Adding a target report to test-suite's Makefile to get a short summary.Gravatar Hugo Herbelin2015-12-02
* Improving syntax of pat/constr introduction pattern so thatGravatar Hugo Herbelin2015-12-02
* Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Gravatar Hugo Herbelin2015-12-02
* Test for bug #4149.Gravatar Pierre-Marie Pédrot2015-11-30
* Test-suite files for closed bugsGravatar Matthieu Sozeau2015-11-28
* Closed bugs.Gravatar Matthieu Sozeau2015-11-28
* Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
* Fixing the "parsing rules with idents later declared as keywords" problem.Gravatar Hugo Herbelin2015-11-26
* Fixing a vm_compute bug in the presence of let-ins among theGravatar Hugo Herbelin2015-11-22
* Fixing a bug of adjust_subst_to_rel_context.Gravatar Hugo Herbelin2015-11-22
* Fixing kernel bug in typing match with let-ins in the arity.Gravatar Hugo Herbelin2015-11-22
* Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.Gravatar Pierre-Marie Pédrot2015-11-19
* Fixing logical bugs in the presence of let-ins in computiong primitiveGravatar Hugo Herbelin2015-11-18
* Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.Gravatar Pierre-Marie Pédrot2015-11-12
* Fixed test-suite file for bug #3998.Gravatar Matthieu Sozeau2015-11-12
* Now closed.Gravatar Matthieu Sozeau2015-11-11
* Fix bug #3257, setoid_reflexivity should fail if not completing the goal.Gravatar Matthieu Sozeau2015-11-11
* Fix bug #4293: ensure let-ins do not contain algebraic universes inGravatar Matthieu Sozeau2015-11-11
* Fixing bug #3554: Anomaly: Anonymous implicit argument.Gravatar Pierre-Marie Pédrot2015-11-11
* Test for bug #4404.Gravatar Pierre-Marie Pédrot2015-11-10
* Fixing output test Existentials.v after eec77191b.Gravatar Hugo Herbelin2015-11-07
* Tests for syntax "Show id" and [id]:tac (shelved or not).Gravatar Hugo Herbelin2015-11-07
* Fixing complexity file f_equal.v.Gravatar Hugo Herbelin2015-11-06
* Fixing complexity issue with f_equal. Thanks to J.-H. JourdanGravatar Hugo Herbelin2015-11-06
* Add test-suite file for #4273.Gravatar Matthieu Sozeau2015-11-05
* Univs: missing checks in evarsolve with candidates and missing aGravatar Matthieu Sozeau2015-11-04
* Hint Cut documentation and cleanup of printing (was duplicated andGravatar Matthieu Sozeau2015-11-04
* Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusionGravatar Matthieu Sozeau2015-11-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 23:15:27 +0000