aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-30Merge branch 'v8.5'Pierre-Marie Pédrot
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-30More uniformity in the style of comparison functions.Arnaud Spiwack
2015-10-29Make the code of compare functions linear in the number of constructors.Arnaud Spiwack
2015-10-29Monotonizing Tactics.change_arg.Pierre-Marie Pédrot
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-29Removing some goal unsafeness in Equality.Pierre-Marie Pédrot
2015-10-29Removing unused and useless exported function in Hints.Pierre-Marie Pédrot
2015-10-29Removing the evar_map argument from s_enter.Pierre-Marie Pédrot
2015-10-29Removing some goal unsafeness in inductive schemes.Pierre-Marie Pédrot
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-29Merge branch 'v8.5'Pierre-Marie Pédrot
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-28Fixing the return type of the Atoken symbol.Pierre-Marie Pédrot
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
2015-10-28Do not pause globing in funind. (Fix bug #4382)Guillaume Melquiond
2015-10-28Type-safe Argextend.Pierre-Marie Pédrot
2015-10-27Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesMatthieu Sozeau
2015-10-27Removing unused code in Pcoq.Pierre-Marie Pédrot
2015-10-27Type-safe Egramml.grammar_prod_item.Pierre-Marie Pédrot
2015-10-27Finer type for Pcoq.interp_entry_name.Pierre-Marie Pédrot
2015-10-27Getting rid of most uses of unsafe_grammar_extend.Pierre-Marie Pédrot
2015-10-27Type-safe Egramml.make_rule.Pierre-Marie Pédrot
2015-10-27Indexing existentially quantified entries returned by interp_entry_name.Pierre-Marie Pédrot
2015-10-27Type-safe grammar extensions.Pierre-Marie Pédrot
2015-10-26Seeing configure as a static resolution of path, hence hardwiring longHugo Herbelin
2015-10-26Fixing bugs in options of the configure.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-17 07:15:08 +0000