aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
2016-04-27Fixing a "This clause is redundant" error when interpreting the "in"Hugo Herbelin
2016-04-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-08Fixing printing of Tactic Notations with tactic arguments.Pierre-Marie Pédrot
2016-04-07An example which failed in 8.5 and that d670c6b6 fixes.Hugo Herbelin
2016-04-05Add -compat 8.4 econstructor tactics, and testsJason Gross
2016-03-28Fixing an incorrect use of prod_appvect on a term which was not aHugo Herbelin
2016-03-25Test suite file for a bug in BigQ arithmetic fixed a while ago.Maxime Dénès
2016-03-18Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-15Fix bug when a sort is ascribed to a RecordMatthieu Sozeau
2016-03-13Adopting the same rules for interpreting @, abbreviations andHugo Herbelin
2016-03-13Adding a file summarizing the inconsistencies in interpreting implicitHugo Herbelin
2016-03-10Primitive projections: protect kernel from erroneous definitions.Matthieu Sozeau
2016-03-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-09Fix strategy of Keyed UnificationMatthieu Sozeau
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-05Using build_selector from Equality as a replacement of the selectorHugo Herbelin
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-02-23Document differences of Hint Resolve and Hint ExternMatthieu Sozeau
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-21Stronger invariants on the use of the introduction pattern (pat1,...,patn).Hugo Herbelin
2016-01-21Fixing some problems with double induction.Hugo Herbelin
2016-02-18Fixing a bug with introduction patterns over inductive types containing let-ins.Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-13Fixing #4467 (continued).Hugo Herbelin
2016-01-12Extend last commit: keyed unification uses full conversions on the applied co...Matthieu Sozeau
2016-01-12Extend Keyed Unification tests with the one from R. Krebbers.Matthieu Sozeau
2015-12-25Fixing a bug in the order of side conditions for introduction pattern -> and <-.Hugo Herbelin
2015-12-25Fixing an "injection as" bug in the presence of side conditions.Hugo Herbelin
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-15Proof using: do not clear unused section hyps automaticallyEnrico Tassi
2015-12-15Fix test-suite files after change in refine tactic.Maxime Dénès
2015-12-15Adding a test for the unshelve tactical.Pierre-Marie Pédrot
2015-12-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-14extraction_impl.v: fix a typoPierre Letouzey
2015-12-14A test file for Extraction Implicit (including bugs #4243 and #4228)Pierre Letouzey
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-10Fixing a pat%constr bug. Thanks to Enrico for reporting.Hugo Herbelin
2015-12-10Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Hugo Herbelin
2015-12-09bug fixes to vm computation + test cases.Gregory Malecha
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-05Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Hugo Herbelin
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-02Improving syntax of pat/constr introduction pattern so thatHugo Herbelin
2015-12-02Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Hugo Herbelin
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-26Fixing the "parsing rules with idents later declared as keywords" problem.Hugo Herbelin
2015-11-26Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 07:09:17 +0000