aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-11-11Fix bug #3998: when using typeclass resolution for conversion, allowMatthieu Sozeau
2015-11-11Fix bug #3735: interpretation of "->" in Program follows the standard one.Matthieu Sozeau
2015-11-11Fix bug #3257, setoid_reflexivity should fail if not completing the goal.Matthieu Sozeau
2015-11-11Fix bug #4293: ensure let-ins do not contain algebraic universes inMatthieu Sozeau
2015-11-11Fixing bug #3554: Anomaly: Anonymous implicit argument.Pierre-Marie Pédrot
2015-11-10Updating test-suite after Bracketing Last Introduction Pattern set byHugo Herbelin
2015-11-10Updating Compat85.v after bd1c97653 on bracketing last or-andHugo Herbelin
2015-11-10Revert "Fixing #1225: we now skip the canonically built binding contexts of"Hugo Herbelin
2015-11-10Fixing #1225: we now skip the canonically built binding contexts ofHugo Herbelin
2015-11-10Listing separately changes from 8.5betas to final 8.5 and furtherHugo Herbelin
2015-11-10Activating bracketing of last or-and introduction pattern by defaultHugo Herbelin
2015-11-10Merge origin/v8.5 into trunkHugo Herbelin
2015-11-10Dead code from the commit having introduced primitive projections (a4043608).Hugo Herbelin
2015-11-10Typo.Hugo Herbelin
2015-11-10Fixing a bug in reporting ill-formed constructor.Hugo Herbelin
2015-11-10Test for bug #4404.Pierre-Marie Pédrot
2015-11-10Fix bug #4404: [remember] gives Error: Conversion test raised an anomaly.Pierre-Marie Pédrot
2015-11-09Pushing the backtrace in conversion anomalies.Pierre-Marie Pédrot
2015-11-08Adapting output test inference.v after c23f0cab6 (experimentingHugo Herbelin
2015-11-07Fixing output test Existentials.v after eec77191b.Hugo Herbelin
2015-11-07Preventing an unwanted warning 5 "this function application is partial"Hugo Herbelin
2015-11-07Implementing assert and cut with LetIn rather than using a beta-redex.Hugo Herbelin
2015-11-07Experimenting printing the type of the defined term of a LetIn whenHugo Herbelin
2015-11-07Adding an amazing property of Prop.Hugo Herbelin
2015-11-07Preservation of the name of evars/goals when applying pose/set/intro/clearbody.Hugo Herbelin
2015-11-07Tests for syntax "Show id" and [id]:tac (shelved or not).Hugo Herbelin
2015-11-07Fixing documention of Add Printing Coercion.Hugo Herbelin
2015-11-07Merge remote-tracking branch 'origin/v8.5' into upstream-trunkHugo Herbelin
2015-11-06Fixed #4407.Pierre Courtieu
2015-11-06Fixing #4406 coqdep: No recursive search of ml (-I).Pierre Courtieu
2015-11-06Fixing complexity file f_equal.v.Hugo Herbelin
2015-11-06More on how to compile doc.Hugo Herbelin
2015-11-06Fixing complexity issue with f_equal. Thanks to J.-H. JourdanHugo Herbelin
2015-11-05Add test-suite file for #4273.Matthieu Sozeau
2015-11-05Fix bug #4273Matthieu Sozeau
2015-11-05Update version numbers and magic numbers for 8.5beta3 release.Maxime Dénès
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-04Checker was forgetting to register global universes introduced by opaqueMatthieu Sozeau
2015-11-04Univs: missing checks in evarsolve with candidates and missing aMatthieu Sozeau
2015-11-04Univs: update refman, better printers for universe contexts.Matthieu Sozeau
2015-11-04Hint Cut documentation and cleanup of printing (was duplicated andMatthieu Sozeau
2015-11-04Univs: compatibility with 8.4.Matthieu Sozeau
2015-11-04Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusionMatthieu Sozeau
2015-11-04Test file for #4397.Maxime Dénès
2015-11-03Update compatibility file for some of bug #4392Jason Gross
2015-11-02Fix bug #4397: refreshing types in abstract_generalize.Matthieu Sozeau
2015-11-02Fix bug #4151: discrepancy between exact and eexact/eassumption.Matthieu Sozeau
2015-11-02Refresh rigid universes as well, and in 8.4 compatibility mode,Matthieu Sozeau
2015-11-02Follow-up fix on Enrico's 6e376c8097d75b6e, with Enrico.Maxime Dénès
2015-11-02Adding syntax "Show id" to show goal named id (shelved or not).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-17 05:44:48 +0000