aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2016-04-15Build stm debugging messages lazily so that they are not silentlyHugo Herbelin
2016-04-15Cleaning unpolished commit 0dfd0fb7d7 on basic functions about union type.Hugo Herbelin
2016-04-14This is an attempt to clarify terminology in choosing variable namesHugo Herbelin
2016-04-14Moving and enhancing the grammar_tactic_prod_item_expr type.Pierre-Marie Pédrot
2016-04-13Uniformizing the semantics of ARGUMENT EXTEND macros.Pierre-Marie Pédrot
2016-04-12Adding toplevel representation sharing for some generic arguments.Pierre-Marie Pédrot
2016-04-12Removing redundant *_TYPED AS clauses in EXTEND statements.Pierre-Marie Pédrot
2016-04-12Adding warnings for inferrable *_TYPED AS clauses.Pierre-Marie Pédrot
2016-04-12Allowing optional RAW_TYPED and GLOB_TYPED clauses in ARGUMENT EXTEND.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 03:14:41 +0000