aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppconstr.ml
Commit message (Expand)AuthorAge
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
* Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Gravatar Hugo Herbelin2018-02-20
* Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-01-30
* Removing cumbersome location in multiple patterns.Gravatar Hugo Herbelin2017-12-12
* Improving spacing in printing disjunctive patterns.Gravatar Hugo Herbelin2017-12-12
* Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
* [parser] Remove unnecessary statically initialized hook.Gravatar Emilio Jesus Gallego Arias2017-11-19
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
* Exporting the level-parametric printer of constr and its variants.Gravatar Hugo Herbelin2017-11-02
* Removing a redundancy in naming types (Ppconstr.precedence = tolerability).Gravatar Hugo Herbelin2017-11-02
* Reporting locations in error messages about notation formats.Gravatar Hugo Herbelin2017-09-18
* Don't exclude a priori CLocalDef to be treated by ppconstr.ml.Gravatar Hugo Herbelin2017-09-12
* A new step of restructuration of notations.Gravatar Hugo Herbelin2017-08-29
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Don't double up on periods in anomaliesGravatar Jason Gross2017-06-02
* Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Allow flexible anonymous universes in instances and sorts.Gravatar Gaetan Gilbert2017-05-03
| * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] More located use.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | [constrexpr] Make patterns use Loc.located for location informationGravatar Emilio Jesus Gallego Arias2017-04-24
|/
* Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
|\
* | Fix higher-order pattern variables not being printed as "@?" (bug #5431).Gravatar Guillaume Melquiond2017-04-02
| * Applying same convention as in Definition for printing type in a let in.Gravatar Hugo Herbelin2017-03-24
| * Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| * Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
|/
* [pp] Move terminal-specific tagging to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Remove unused printing tagging infrastructure.Gravatar Emilio Jesus Gallego Arias2017-03-21
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-01-23
|\
| * Fixing a little bug in printing cofix with no arguments.Gravatar Hugo Herbelin2017-01-05
* | [toplevel] Remove duplicate beautify flags.Gravatar Emilio Jesus Gallego Arias2016-10-17
* | Moving Pp.comments to CLexer so that Pp is purer (no more side-effectGravatar Hugo Herbelin2016-10-09
* | Fixing a beautifier bug pointed out by Emilio.Gravatar Hugo Herbelin2016-10-05
* | Fix bug #4869, allow Prop, Set, and level names in constraints.Gravatar Matthieu Sozeau2016-09-29
* | Fix tagging of notations.Gravatar Pierre-Marie Pédrot2016-08-29
* | 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
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03