aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
* Properly parenthesize "ltac:" arguments (bug #5169).Gravatar Guillaume Melquiond2016-11-22
* Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Gravatar Maxime Dénès2016-11-18
* [stm] Remove STM-related vernacularsGravatar Emilio Jesus Gallego Arias2016-11-17
* Merge remote-tracking branch 'github/pr/339' into v8.6Gravatar Maxime Dénès2016-11-07
|\
* | Do not print dependent evars by default (expensive)Gravatar Matthieu Sozeau2016-11-05
| * Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
|/
* Merge remote-tracking branch 'github/pr/337' into v8.6Gravatar Maxime Dénès2016-10-28
|\
| * Complete overhaul of the Arguments vernacular.Gravatar Maxime Dénès2016-10-27
* | Refine printing of pending unification constraintsGravatar Matthieu Sozeau2016-10-20
* | [toplevel] Remove duplicate beautify flags.Gravatar Emilio Jesus Gallego Arias2016-10-17
|/
* Fixing a few confusions on the name of the beautify flag.Gravatar Hugo Herbelin2016-10-12
* Moving Pp.comments to CLexer so that Pp is purer (no more side-effectGravatar Hugo Herbelin2016-10-09
* Fix bug #5098: Symmetry broken in HoTT.Gravatar Pierre-Marie Pédrot2016-10-08
* Fixing a beautifier bug pointed out by Emilio.Gravatar Hugo Herbelin2016-10-05
* Merge remote-tracking branch 'github/pr/305' into v8.6Gravatar Maxime Dénès2016-10-04
|\
* | Fix bug #4661: Cannot mask the absolute name.Gravatar Pierre-Marie Pédrot2016-10-01
| * Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Gravatar Guillaume Melquiond2016-10-01
|/
* Merge remote-tracking branch 'github/pr/299' into v8.6Gravatar Maxime Dénès2016-09-30
|\
* | Fix bug #4798: compat notations should not modify the parser.Gravatar Pierre-Marie Pédrot2016-09-29
* | Arguments: cleanup + detect discrepancy rename/implicit (#3753)Gravatar Enrico Tassi2016-09-29
| * Fix bug #4869, allow Prop, Set, and level names in constraints.Gravatar Matthieu Sozeau2016-09-29
|/
* Moving "move" in the new proof engine.Gravatar Hugo Herbelin2016-09-24
* Addressing OCaml compilation warnings.Gravatar Hugo Herbelin2016-09-16
* Fix bug #4940: Tactic notation printing could be more informative.Gravatar Pierre-Marie Pédrot2016-09-09
* Fix tagging of notations.Gravatar Pierre-Marie Pédrot2016-08-29
* Support qualified identifiers in Show Match (bug #5050).Gravatar Guillaume Melquiond2016-08-27
* Complementing previous commit on fixes for printing binding patterns.Gravatar Hugo Herbelin2016-07-19
* Some extra fixes in printing patterns in binders.Gravatar Hugo Herbelin2016-07-19
* Taking into account binding patterns when agglutinating sequences of binders.Gravatar Hugo Herbelin2016-07-19
* Fixing missing parentheses in printing of patterns in binders.Gravatar Hugo Herbelin2016-07-19
* primproj: warning and avoid error.Gravatar Matthieu Sozeau2016-07-06
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
* Merge remote-tracking branch 'github/pr/207' into trunkGravatar Maxime Dénès2016-06-28
|\
* | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| * Add [Unset Printing Dependent Evars Line]Gravatar Jason Gross2016-06-19
|/
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* Print the type-in-type flag in various user-facing functions.Gravatar Pierre-Marie Pédrot2016-06-18
* Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
* Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
* proof mode: print unification constraintsGravatar Matthieu Sozeau2016-06-16
* Extend Hint Mode to handle the no-head-evar caseGravatar Matthieu Sozeau2016-06-16
* Isolating and exporting a function for printing body of a recursive definition.Gravatar Hugo Herbelin2016-06-16
* Simplification in ppvernac.ml.Gravatar Hugo Herbelin2016-06-16
* Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.Gravatar Hugo Herbelin2016-06-16
* Fixing extra space in printing bullets.Gravatar Hugo Herbelin2016-06-16
* Fixing space in printing <+ and <: + fixing missing Inline keyword.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of Instance.Gravatar Hugo Herbelin2016-06-16
* Fixing extra space in printing abbreviations (SyntaxDefinition).Gravatar Hugo Herbelin2016-06-16
* Fixing printing of Polymorphic/Monomorphic.Gravatar Hugo Herbelin2016-06-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 07:52:33 +0000