aboutsummaryrefslogtreecommitdiff
path: root/printing/ppconstr.ml
AgeCommit message (Expand)Author
2017-01-05Fixing a little bug in printing cofix with no arguments.Hugo Herbelin
2016-10-17[toplevel] Remove duplicate beautify flags.Emilio Jesus Gallego Arias
2016-10-09Moving Pp.comments to CLexer so that Pp is purer (no more side-effectHugo Herbelin
2016-10-05Fixing a beautifier bug pointed out by Emilio.Hugo Herbelin
2016-09-29Fix bug #4869, allow Prop, Set, and level names in constraints.Matthieu Sozeau
2016-08-29Fix tagging of notations.Pierre-Marie Pédrot
2016-07-19Complementing previous commit on fixes for printing binding patterns.Hugo Herbelin
2016-07-19Some extra fixes in printing patterns in binders.Hugo Herbelin
2016-07-19Taking into account binding patterns when agglutinating sequences of binders.Hugo Herbelin
2016-07-19Fixing missing parentheses in printing of patterns in binders.Hugo Herbelin
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-27Adding ability to put any pattern in binders, prefixed by a quote.Daniel de Rauglaudre
2016-06-16Fixing printing of Instance.Hugo Herbelin
2016-04-27Revert "A heuristic to add parentheses in the presence of rules such as"Hugo Herbelin
2016-04-27Revert "Temporary deactivate re-interpretation of terms in beautify."Hugo Herbelin
2016-04-27Revert "Fixing printing of Instance."Hugo Herbelin
2016-04-27Fixing printing of Instance.Hugo Herbelin
2016-04-27Temporary deactivate re-interpretation of terms in beautify.Hugo Herbelin
2016-04-27A heuristic to add parentheses in the presence of rules such asHugo Herbelin
2016-03-13Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Hugo Herbelin
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: removing unused fieldMatej Kosik
2016-01-02Remove some unused functions.Guillaume Melquiond
2015-12-22Do not compose "str" and "to_string" whenever possible.Guillaume Melquiond
2015-12-18CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedMatej Kosik
2015-12-03Improving over printing of let-tuple (see #4447).Hugo Herbelin
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-06-24Add a space in cast since cast binds loosely.Gregory Malecha
2015-01-12Update headers.Maxime Dénès
2014-11-30Fixing printing of dirpathes in Ppconstr. It was reversed.Pierre-Marie Pédrot
2014-11-25Adding tag output to references in Ppconstr.Pierre-Marie Pédrot
2014-11-17Adding notation terminals to coqtop highlight.Pierre-Marie Pédrot
2014-11-17Fixing semantics of Ppconstr.print_hunks.Pierre-Marie Pédrot
2014-11-17Missing keywords in Ppconstr.Pierre-Marie Pédrot
2014-11-17Moving printing code for red_expr and may_eval to Pptactic.Pierre-Marie Pédrot
2014-11-17Default styles for printing tags.Pierre-Marie Pédrot
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-15Additional style tags for constrs.Pierre-Marie Pédrot
2014-11-15Setting a keyword tag in Ppconstr.Pierre-Marie Pédrot
2014-11-10Plug the dynamic tags in the Richpp mechanism.Pierre-Marie Pédrot
2014-11-05lib/RichPp: Rename into Richpp.Yann Régis-Gianas
2014-11-04lib/Ppconstr: Cosmetics.Regis-Gianas
2014-11-04lib/Pp.tag: New.Regis-Gianas
2014-11-04printing/Ppannotation: Introduce a new annotation for keywords.Regis-Gianas
2014-11-04Ppannotation: New.Regis-Gianas
2014-11-04printing/Ppconstr.Make:Regis-Gianas
2014-11-04printing/Ppconstr.print_hunks:Regis-Gianas
2014-11-04printing/Ppconstr: Cosmetics.Regis-Gianas
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:38:02 +0000