aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-11-07Fixing documention of Add Printing Coercion.Hugo 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-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
2015-11-02Made that the syntax [id]:tac also applies to the shelve, which is after all ...Hugo Herbelin
2015-11-02STM: fix undo into a branch containing side effectsEnrico Tassi
2015-11-02STM: never reopen a branch containing side effectsEnrico Tassi
2015-10-30Command.declare_definition: grab the fix_exn early (follows 77cf18e)Enrico Tassi
2015-10-30Manually expand red_tactic so that notations do not break reduction tactics. ...Guillaume Melquiond
2015-10-30Add a way to get the right fix_exn in external vernacular commandsMatthieu Sozeau
2015-10-30Fix typo.Guillaume Melquiond
2015-10-29Handle side-effects of Vernacular commands inside proofs better, so thatMatthieu Sozeau
2015-10-29Collect subproof universes in handle_side_effects.Matthieu Sozeau
2015-10-29Manually expand the debugging versions of "trivial" and "auto". (Fix bug #4392)Guillaume Melquiond
2015-10-29Avoid an anomaly when destructing an unknown ident. (Fix bug #4395)Guillaume Melquiond
2015-10-29Fixing another instance of bug #3267 in eauto, this time in theHugo Herbelin
2015-10-29Cleanup API and comments of 908dcd613Enrico Tassi
2015-10-29Accept option -compat 8.5. (Fix bug #4393)Guillaume Melquiond
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-28Printing of @{} instances for polymorphic references in Print and About.Matthieu Sozeau
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-28lib_stack: API to reorder the libstackEnrico Tassi
2015-10-28Fix test suite after Matthieu's ed7af646f2e486b.Maxime Dénès
2015-10-28Fix bug in native compiler with universe polymorphism.Maxime Dénès
2015-10-28Refine Gregory Malecha's patch on VM and universe polymorphism.Maxime Dénès
2015-10-28Conversion of polymorphic inductive types was incomplete in VM and native.Maxime Dénès
2015-10-28Fix minor typo in native compiler.Maxime Dénès
2015-10-28test cases.Gregory Malecha
2015-10-28Adds support for the virtual machine to perform reduction of universe polymor...Gregory Malecha
2015-10-28Univs: fix bug #4375, accept universe binders on (co)-fixpointsMatthieu Sozeau
2015-10-28Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins"Hugo Herbelin
2015-10-28Seeing configure as a static resolution of path continued (not yet on windows).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 06:35:11 +0000