aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-11-15Adding a command line option to print out accepted color tags.Pierre-Marie Pédrot
2014-11-15Additional style tags for constrs.Pierre-Marie Pédrot
2014-11-15Reworking the -color flag of coqtop.Pierre-Marie Pédrot
2014-11-15Removing deprecated code handling color in Pp.Pierre-Marie Pédrot
2014-11-15Setting a keyword tag in Ppconstr.Pierre-Marie Pédrot
2014-11-15Plugging the color initialization in the Coqtop loop.Pierre-Marie Pédrot
2014-11-15Adding a pretty-printing style library.Pierre-Marie Pédrot
2014-11-15Adding a terminal library.Pierre-Marie Pédrot
2014-11-14Use return code to classify anomalies as active open bugs.Xavier Clerc
2014-11-14Exit with code 129 when an anomaly occurs.Xavier Clerc
2014-11-14Get rif of exit codes 120, 121, 123, and 124.Xavier Clerc
2014-11-14Add missing "Fail" to test case for bug #2814.Xavier Clerc
2014-11-14Reproduction cases for the test suite.Xavier Clerc
2014-11-14Preserving the good effect of 014e5ac92a on not leaving dangling localHugo Herbelin
2014-11-13Fixing Scheme Equality, after bug introduced in bf018569405c.Hugo Herbelin
2014-11-13Move conjugate_verb_to_be next to cString.plural.Hugo Herbelin
2014-11-13Removing yet another source of remaining local definitions.Hugo Herbelin
2014-11-12Document (some) Proof using syntax + the new Optimize commandsEnrico Tassi
2014-11-12Cleaner interfaces for linking locations of native compiler.Maxime Dénès
2014-11-11Accepting conversion on inner closed subterms while looking forHugo Herbelin
2014-11-11Adapting output tests to current naming of evars, even if unclearHugo Herbelin
2014-11-11Updating CHANGES (evars as ident).Hugo Herbelin
2014-11-11American spelling + layout in CHANGES.Hugo Herbelin
2014-11-11Renouncing to check only at the end of the call to "apply in" theHugo Herbelin
2014-11-10Universes.nf_evars_and_universes_opt_subst substitutes evars eagerly.Pierre-Marie Pédrot
2014-11-10Evar normalization is now done eagerly.Pierre-Marie Pédrot
2014-11-10Fix #3282: VM confused by let bindings in fixpoints.Maxime Dénès
2014-11-10Better printing of dynlink errors in native compiler.Maxime Dénès
2014-11-10Plug the dynamic tags in the Richpp mechanism.Pierre-Marie Pédrot
2014-11-10Adding a dynamic tag type in Pp.Pierre-Marie Pédrot
2014-11-10Replugging hints in rewriting strategies.Pierre-Marie Pédrot
2014-11-10Fixing wrongly used tclWITHHOLES in named tactics (continuation of 9fa45b3).Pierre-Marie Pédrot
2014-11-09Fixing bug #3803.Pierre-Marie Pédrot
2014-11-09Removing the unused boolean flag from the move tactic implementation.Pierre-Marie Pédrot
2014-11-09Removing a unused boolean in the TacMove node of tacexpr AST.Pierre-Marie Pédrot
2014-11-09Adding test for bug 3792.Pierre-Marie Pédrot
2014-11-09Fixing bug #3792.Pierre-Marie Pédrot
2014-11-09new: Optimize Proof, Optimize HeapEnrico Tassi
2014-11-08Follow up to experimental eager evar unification in bcba6d1bc9:Hugo Herbelin
2014-11-08Fixing a bug in change of subst_defined_metas in bcba6d1bc9f769da:Hugo Herbelin
2014-11-08Continuing 3741c46fe134 on reporting ltac error.Hugo Herbelin
2014-11-08Compatibility with 8.4 in the heuristic used to build the inductionHugo Herbelin
2014-11-08Test #3655 was failing due to an anomaly. Now it rather has to failHugo Herbelin
2014-11-08Test fixed by PMP's commits from Oct 21.Hugo Herbelin
2014-11-07Fixing doc of Functional Induction.Hugo Herbelin
2014-11-07Fixing Functional Induction when applied to an alias (reference manualHugo Herbelin
2014-11-07Granting #3717 (more informative error message on missing arguments for funct...Hugo Herbelin
2014-11-07Test for #3675 on primitive projections.Hugo Herbelin
2014-11-07Fixing #3562 ("as" in "destruct" expects either a disjunctiveHugo Herbelin
2014-11-07Test for #3542 fixed some time ago.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 00:14:46 +0000