aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-04-27Protect printing of ltac's "context [...]" from possible collisionHugo Herbelin
2016-04-27Protect printing of intro-patterns from collision when "[|" or "|]"Hugo Herbelin
2016-04-27Fixing parsing of constr argument of ltac functions at level 8 in theHugo Herbelin
2016-04-27Fixing printing of keeping hyp on the fly.Hugo Herbelin
2016-04-27Fixing printing of inversion as.Hugo Herbelin
2016-04-27Fixing extra space in printing destruct/induction as.Hugo Herbelin
2016-04-27Fixing printing of induction/destruct as.Hugo Herbelin
2016-04-27Fixing printing of pat%constr.Hugo Herbelin
2016-04-27Fixing printers for pr_auto_using and pr_firstorder_using.Hugo Herbelin
2016-04-27In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.Hugo Herbelin
2016-04-27Adding option "Set Reversible Pattern Implicit" to Specif.v so that anHugo Herbelin
2016-04-27Honor parsing and printing levels for tactic entry in TACTIC EXTEND andHugo Herbelin
2016-04-27Temporary deactivate re-interpretation of terms in beautify.Hugo Herbelin
2016-04-27Being defensive in printing implicit arguments also with manualHugo Herbelin
2016-04-27In the short term, stronger invariant on the syntax of TacAssert, whatHugo Herbelin
2016-04-27Changing rule for "*" in Operator_Properties so that, iterated, itHugo Herbelin
2016-04-27Protect the beautifier from change in the lexer state (typically byHugo Herbelin
2016-04-27So as to beautify to work, do not use notations in Inductive typesHugo Herbelin
2016-04-27Adding a target check-beautify for testing reparsability ofHugo Herbelin
2016-04-27Adding a target for beautification.Hugo Herbelin
2016-04-27Not taking arguments given by name or position into account whenHugo Herbelin
2016-04-27A heuristic to add parentheses in the presence of rules such asHugo Herbelin
2016-04-27Fixing a "This clause is redundant" error when interpreting the "in"Hugo Herbelin
2016-04-27Reformatting + removal of some useless data + some cut-eliminationHugo Herbelin
2016-04-27Attempt to slightly improve abusive "Collision between boundHugo Herbelin
2016-04-25Removing dead code in Compat.Pierre-Marie Pédrot
2016-04-25Simplifying and uniformizing the implementation of tactic notations.Pierre-Marie Pédrot
2016-04-25Removing dead code related to printing of ML tactics in Pptactic.Pierre-Marie Pédrot
2016-04-25Merging the ML tactic notation and plain Tactic Notation mechanisms.Pierre-Marie Pédrot
2016-04-25Factorizing code in tactic notations.Pierre-Marie Pédrot
2016-04-25Documenting API.Pierre-Marie Pédrot
2016-04-24Remove dead registering code in Pcoq.Pierre-Marie Pédrot
2016-04-24Disentangle tactic notation resolution from Pcoq.Pierre-Marie Pédrot
2016-04-24Higher-level API for tactic notations.Pierre-Marie Pédrot
2016-04-24Factorizing the declaration of ML notation printing in Tacentries.Pierre-Marie Pédrot
2016-04-24Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-22Fixing output test Notations2.Hugo Herbelin
2016-04-22Mention problems with fix of #4582 in CHANGES.Maxime Dénès
2016-04-22Mention #4548 (fixed) in CHANGES.Maxime Dénès
2016-04-20Adding an OCaml printer for pre-initialization anomalies.Pierre-Marie Pédrot
2016-04-19Do that "make" in test-suite writes failures as a default togetherHugo Herbelin
2016-04-19Fixing #4677 (collision of a global variable and of a local variableHugo Herbelin
2016-04-19Fixing 50266aab on incompatibility of OCaml 4.01.0 with option -debug.Hugo Herbelin
2016-04-19Revert "Fixing printing of surrounding parentheses in "ltac:"."Hugo Herbelin
2016-04-18Bugfix micromega: more careful syntaxification of terms of the form (Rinv t)Frédéric Besson
2016-04-17Building lazily a few debugging messages involving expressions of commandsHugo Herbelin
2016-04-17Updating configure.ml wrt Coq not compilable with OCaml 4.01.0 in debug mode.Hugo Herbelin
2016-04-17Fixing printing of surrounding parentheses in "ltac:".Hugo Herbelin
2016-04-17Updating OCaml version number needed for 8.6.Hugo Herbelin
2016-04-17Add changelog for 8.5pl1 after the fact.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-04 18:12:15 +0000