aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2016-09-09no-refold patchPaul Steckler
2016-09-09Fix output test-suite after commit 0d3c319.Pierre-Marie Pédrot
2016-09-09Update csdp cache.Pierre-Marie Pédrot
2016-09-08Fix Bug #5073 : regression of micromega pluginFrédéric Besson
2016-09-08Fix Bug #5073 : regression of micromega pluginFrédéric Besson
2016-09-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-07micromega : more robust generation of proof termsFrédéric Besson
2016-09-05Test file for #5065 - Anomaly: Not a proof by inductionMaxime Dénès
2016-09-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-02Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-01Fix test-suite after Frédéric's 6231f07b2.Maxime Dénès
2016-08-31Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.Frédéric Besson
2016-08-31Fix bug #5043: [Admitted] lemmas pick up section variables.Pierre-Marie Pédrot
2016-08-30Fixing output test-suite after warning for inner Requires.Pierre-Marie Pédrot
2016-08-30Fix bug #4893: not_evar: unexpected failure in 8.5pl1.Pierre-Marie Pédrot
2016-08-30plugin micromega : nra also handles non-linear rational arithmetic over Q (Fi...Frédéric Besson
2016-08-30Fix bug #3920: eapply masks an hypothesis name.Pierre-Marie Pédrot
2016-08-28Fix bug #4764: Syntactic notation externalization breaks.Pierre-Marie Pédrot
2016-08-25Merge remote-tracking branch 'v8.6' into trunkMatej Kosik
2016-08-23Fix bug #4904: [Import] does not load intermediately unqualified names of ali...Pierre-Marie Pédrot
2016-08-21Merge branch 'v8.6'Pierre-Marie Pédrot
2016-08-21Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-08-20Fixing an anomaly in printing a unification error message.Hugo Herbelin
2016-08-19Test file for bug #4187.Pierre-Marie Pédrot
2016-08-19Merge remote-tracking branch 'origin/pr/246' into v8.6Matthieu Sozeau
2016-08-18Adding a test for bug #4653.Pierre-Marie Pédrot
2016-08-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-08-17Fixing #3070 ("subst" taking properly into account chains of dependencies).Hugo Herbelin
2016-08-16Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-29Fix bug #4673: regression in setoid_rewrite.Matthieu Sozeau
2016-07-29Merge remote-tracking branch 'gforge/v8.5' into v8.6Matthieu Sozeau
2016-07-29Fix bug #3886, generation of obligations of fixesMatthieu Sozeau
2016-07-29Fix #4769, univ poly and elim schemes in sectionsMatthieu Sozeau
2016-07-26Merge branch 'v8.6' into trunkPierre Letouzey
2016-07-26Fix bug #4754, allow conversion problems to remainMatthieu Sozeau
2016-07-21Fix bug #4679, weakened setoid_rewrite unificationMatthieu Sozeau
2016-07-20Merge branch 'v8.6'Pierre-Marie Pédrot
2016-07-20Fix bug #4780: universe leak in letin_tacMatthieu Sozeau
2016-07-20Fix bug #4780: universe leak in letin_tacMatthieu Sozeau
2016-07-19Fix Errors.out missing a dot...Matthieu Sozeau
2016-07-19Some extra fixes in printing patterns in binders.Hugo Herbelin
2016-07-19Taking into account binding patterns when agglutinating sequences of binders.Hugo Herbelin
2016-07-19Fixing missing parentheses in printing of patterns in binders.Hugo Herbelin
2016-07-19Notations: fixing multiple binders used as terms in reverse order.Hugo Herbelin
2016-07-19Removing a source of clash with multiple recursive patterns in notations.Hugo Herbelin
2016-07-18A new step on using alpha-conversion in printing notations.Hugo Herbelin
2016-07-18Marking bug #3383 as solved.Pierre-Marie Pédrot
2016-07-18Fix bug #4923: Warning: appcontext is deprecated.Pierre-Marie Pédrot
2016-07-17Partial fix to #4592 (notation requiring alpha-conversion for printing).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-11 17:43:25 +0000