aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-11-18Fixing detection of occurrences in the presence of nested subterms forHugo Herbelin
2014-11-18Clarifying the role of ListSet.v in the library, compared to otherHugo Herbelin
2014-11-17Adding notation terminals to coqtop highlight.Pierre-Marie Pédrot
2014-11-17Fixing semantics of Ppconstr.print_hunks.Pierre-Marie Pédrot
2014-11-17Missing keywords in Ppconstr.Pierre-Marie Pédrot
2014-11-17Setting printing tags for Ltac.Pierre-Marie Pédrot
2014-11-17Moving printing code for red_expr and may_eval to Pptactic.Pierre-Marie Pédrot
2014-11-17Documenting the -color option.Pierre-Marie Pédrot
2014-11-17Documenting use of colors in Coq.Pierre-Marie Pédrot
2014-11-17Default styles for printing tags.Pierre-Marie Pédrot
2014-11-17Setting error tag on generic errors returned by Coqtop.Pierre-Marie Pédrot
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-16Fixing side bug in db37c9f3f32ae7 delaying interpretation of theHugo Herbelin
2014-11-16For consistency with other coqtop flags, use -help rather than --help in usage.Hugo Herbelin
2014-11-15Adding tags to messages.Pierre-Marie Pédrot
2014-11-15Removing a pperrnl.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 20:13:01 +0000