aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-04-27Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.Hugo Herbelin
2016-04-27Fixing extra space in printing bullets.Hugo Herbelin
2016-04-27Fixing space in printing <+ and <: + fixing missing Inline keyword.Hugo Herbelin
2016-04-27Fixing printing of Instance.Hugo Herbelin
2016-04-27Fixing extra space in printing abbreviations (SyntaxDefinition).Hugo Herbelin
2016-04-27Fixing printing of Polymorphic/Monomorphic.Hugo Herbelin
2016-04-27Fixing printing of Arguments.Hugo Herbelin
2016-04-27Printing notations as parsed.Hugo Herbelin
2016-04-27Revert "Protect printing of intro-patterns from collision when "[|" orHugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 15:07:45 +0000