aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
2015-09-17Merge branch 'v8.5' into trunkMaxime Dénès
2015-09-16In pat/constr introduction patterns, fixing in a better way clearing problemsHugo Herbelin
2015-09-09Merge remote-tracking branch 'origin/v8.5' into trunkHugo Herbelin
2015-09-08Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commitsHugo Herbelin
2015-09-08Ensuring that patterns of the form pat/constr move the hypotheses replacingHugo Herbelin
2015-09-08Documenting the new behaviour of the Shrink Obligations flag.Pierre-Marie Pédrot
2015-08-22Documenting the Shrink Abstract option.Pierre-Marie Pédrot
2015-08-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-08-02Continuing 817308ab (use ltac env for terms in ltac context) + fixHugo Herbelin
2015-08-02Fixing test apply.v (had wrong option name).Hugo Herbelin
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02Fixing test apply.v (had wrong option name).Hugo Herbelin
2015-08-02Fixing #4221 (interpreting bound variables using ltac env was possiblyHugo Herbelin
2015-08-02Granting Jason's request for an ad hoc compatibility option onHugo Herbelin
2015-07-27Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-27Add an Iterative Deepening search strategy to typeclass resolution.Matthieu Sozeau
2015-07-22Extraction: fix primitive projection extraction.Matthieu Sozeau
2015-07-18Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-07Univs: bug fix.Matthieu Sozeau
2015-07-02Remove a line from test-suite.Maxime Dénès
2015-06-30Another missing Fail and comment in test-suite.Maxime Dénès
2015-06-30Missing "Fail" in test-suite.Maxime Dénès
2015-06-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-28Fix incompleteness of conversion used by evarconvMatthieu Sozeau
2015-06-24Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-23Fixing incompatibility introduced with simpl in commit 364decf59c1 (orHugo Herbelin
2015-05-15Turning "Set Regular Subst Tactic" on by default (for 8.6).Hugo Herbelin
2015-05-15Merge v8.5 into trunkHugo Herbelin
2015-05-12Extraction: fix the detection of the "polyprop" situationPierre Letouzey
2015-05-09Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default).Hugo Herbelin
2015-05-06Fixing treatment of recursive equations damaged by 857e82b2ca0d1.Hugo Herbelin
2015-04-09Merge branch 'v8.5' into trunkPierre Letouzey
2015-04-01Fixing test-suite.Pierre-Marie Pédrot
2015-03-30Merge branch 'v8.5' into trunkEnrico Tassi
2015-03-25Fully fixing bug #3491 (anomaly when building _rect scheme in theHugo Herbelin
2015-03-25Another example about the consequence of a wrong computation of theHugo Herbelin
2015-03-24Fixing computation of non-recursively uniform arguments in theHugo Herbelin
2015-03-24Fixing wrong rel_context in checking positivity condition.Hugo Herbelin
2015-03-23Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-22Qed export -> Qed exportingEnrico Tassi
2015-03-13Merge branch 'v8.5' into trunkArnaud Spiwack
2015-03-13Add some tests for tryifJason Gross
2015-03-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-03-04Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-03Add a test-suite file ensuring coinductives with primitive projectionsMatthieu Sozeau
2015-02-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-27Fixing first part of bug #3210 (inference of pattern-matching returnHugo Herbelin
2015-02-24Other tests for decl mode, coming from reference manual.Hugo Herbelin
2015-02-23Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 06:15:11 +0000