aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-05-02Generate parsing rules for ML tactics in the same order as before a7917a32.Pierre-Marie Pédrot
2016-05-02Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-02Useless code in Tacentries.Pierre-Marie Pédrot
2016-04-29Reduce ide/coq.png to 256x256.Guillaume Melquiond
2016-04-29Fix incorrect cbv reduction of primitive projections. (Bug #4634)Guillaume Melquiond
2016-04-28Make the language grammar much more precise. (Fix bugs #4682 and #4683)Guillaume Melquiond
2016-04-28Update tutorial (fix bug #4699).Guillaume Melquiond
2016-04-28Fix missing newline in coqchk engagement (bug #4694).Guillaume Melquiond
2016-04-28An example for cd139311e, showing a consequence of not convertingHugo Herbelin
2016-04-27Revert "A heuristic to add parentheses in the presence of rules such as"Hugo Herbelin
2016-04-27Revert "Not taking arguments given by name or position into account when"Hugo Herbelin
2016-04-27Revert "Adding a target for beautification."Hugo Herbelin
2016-04-27Revert "Adding a target check-beautify for testing reparsability of"Hugo Herbelin
2016-04-27Revert "So as to beautify to work, do not use notations in Inductive types"Hugo Herbelin
2016-04-27Revert "Protect the beautifier from change in the lexer state (typically by"Hugo Herbelin
2016-04-27Revert "Changing rule for "*" in Operator_Properties so that, iterated, it"Hugo Herbelin
2016-04-27Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Hugo Herbelin
2016-04-27Revert "Being defensive in printing implicit arguments also with manual"Hugo Herbelin
2016-04-27Revert "Temporary deactivate re-interpretation of terms in beautify."Hugo Herbelin
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
2016-04-27Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"Hugo Herbelin
2016-04-27Revert "In NMake_gen, giving to tactic do_size a grammar rule which respects ...Hugo Herbelin
2016-04-27Revert "Fixing printers for pr_auto_using and pr_firstorder_using."Hugo Herbelin
2016-04-27Revert "Fixing printing of pat%constr."Hugo Herbelin
2016-04-27Revert "Fixing printing of induction/destruct as."Hugo Herbelin
2016-04-27Revert "Fixing extra space in printing destruct/induction as."Hugo Herbelin
2016-04-27Revert "Fixing printing of inversion as."Hugo Herbelin
2016-04-27Revert "Fixing printing of keeping hyp on the fly."Hugo Herbelin
2016-04-27Revert "Fixing parsing of constr argument of ltac functions at level 8 in the"Hugo Herbelin
2016-04-27Revert "Protect printing of intro-patterns from collision when "[|" or "|]""Hugo Herbelin
2016-04-27Revert "Protect printing of ltac's "context [...]" from possible collision"Hugo Herbelin
2016-04-27Revert "Revert "Protect printing of intro-patterns from collision when "[|" or"Hugo Herbelin
2016-04-27Revert "Printing notations as parsed."Hugo Herbelin
2016-04-27Revert "Fixing printing of Arguments."Hugo Herbelin
2016-04-27Revert "Fixing printing of Polymorphic/Monomorphic."Hugo Herbelin
2016-04-27Revert "Fixing extra space in printing abbreviations (SyntaxDefinition)."Hugo Herbelin
2016-04-27Revert "Fixing printing of Instance."Hugo Herbelin
2016-04-27Revert "Fixing space in printing <+ and <: + fixing missing Inline keyword."Hugo Herbelin
2016-04-27Revert "Fixing extra space in printing bullets."Hugo Herbelin
2016-04-27Revert "Removing unused generalization of pr_vernac over pr_constr and pr_lco...Hugo Herbelin
2016-04-27Revert "Simplification in ppvernac.ml."Hugo Herbelin
2016-04-27Revert "Isolating and exporting a function for printing body of a recursive d...Hugo Herbelin
2016-04-27Revert "Fixing printing of Function."Hugo Herbelin
2016-04-27Revert "Adding printers for ring and field commands."Hugo Herbelin
2016-04-27Revert "Fixing Add Parametric Relation by adding printer for binders."Hugo Herbelin
2016-04-27Revert "Fixing printing of Register retroknowledge."Hugo Herbelin
2016-04-27Revert "A fix to #3709: ensuring extra parentheses when a tactic entry has a"Hugo Herbelin
2016-04-27Revert "Passing around the precedence to the generic printer so as to solve"Hugo Herbelin
2016-04-27Revert "Temporary hack to compensate missing comma while re-printing tactic"Hugo Herbelin
2016-04-27Revert "Temporary hack to restore missing printing of "constr:" in right-hand"Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-08 01:44:59 +0000