aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Adding a test for the behaviour of open_constr described in #3777.Gravatar Pierre-Marie Pédrot2016-03-03
* Fixing bug #4596: [rewrite] broke in the past few weeks.Gravatar Pierre-Marie Pédrot2016-02-28
* Document differences of Hint Resolve and Hint ExternGravatar Matthieu Sozeau2016-02-23
* Fixing bug #4580: [Set Refine Instance Mode] also used for Program Instance.Gravatar Pierre-Marie Pédrot2016-02-19
* Fixing bug #4582: cannot override notation [ x ].Gravatar Pierre-Marie Pédrot2016-02-19
* STM: Print/Extraction have to be skipped if -quickGravatar Enrico Tassi2016-02-19
* Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").Gravatar Pierre-Marie Pédrot2016-02-17
* Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
* Adding a test for bug #4378.Gravatar Pierre-Marie Pédrot2016-01-24
* Fixing bug #4495: Failed assertion in metasyntax.ml.Gravatar Pierre-Marie Pédrot2016-01-24
* Fixing bug #4511: evar tactic can create non-typed evars.Gravatar Pierre-Marie Pédrot2016-01-24
* Fix bug #4503: mixing universe polymorphic and monomorphicGravatar Matthieu Sozeau2016-01-23
* Fix bug #4519: oops, global shadowed local universe level bindings.Gravatar Matthieu Sozeau2016-01-23
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fix bug #4420: check_types was losing universe constraints.Gravatar Matthieu Sozeau2016-01-19
* Fixing success of test for #3848 after move to directory "closed".Gravatar Hugo Herbelin2016-01-13
* Fixing #4467 (continued).Gravatar Hugo Herbelin2016-01-13
* Fixing #4467 (missing shadowing of variables in cases pattern).Gravatar Hugo Herbelin2016-01-12
* Fixing #4256 and #4484 (changes in evar-evar resolution made that newGravatar Hugo Herbelin2016-01-12
* Extend last commit: keyed unification uses full conversions on the applied co...Gravatar Matthieu Sozeau2016-01-12
* Extend Keyed Unification tests with the one from R. Krebbers.Gravatar Matthieu Sozeau2016-01-12
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-18 13:47:21 +0000