aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppconstr.ml
Commit message (Expand)AuthorAge
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
* [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
* [api] Move universe syntax to `Glob_term`Gravatar Emilio Jesus Gallego Arias2018-05-08
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* \ Merge PR #6736: [toplevel] Move beautify to its own pass.Gravatar Maxime Dénès2018-03-04
|\ \
| * | [toplevel] Move beautify to its own pass.Gravatar Emilio Jesus Gallego Arias2018-02-28
* | | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
|/ /
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [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