aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/namegen.ml
Commit message (Expand)AuthorAge
* Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
* Merge PR #6899: [compat] Remove "Standard Proposition Elimination"Gravatar Maxime Dénès2018-03-08
|\
* \ Merge PR #6582: Mangle auto-generated namesGravatar Maxime Dénès2018-03-08
|\ \
| | * [compat] Remove "Standard Proposition Elimination"Gravatar Emilio Jesus Gallego Arias2018-03-03
* | | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |/ |/|
| * Implement name mangling optionGravatar Jasper Hugunin2018-02-17
|/
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Fixing a cause of failure of evar_map printer in debugger.Gravatar Hugo Herbelin2017-11-05
* Fixing #5401 (printing of patterns with bound anonymous variables).Gravatar Hugo Herbelin2017-10-28
* Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type "_som...Gravatar Maxime Dénès2017-10-06
|\
| * Fixing BZ#5769 (variable of type "_something" was named after invalid "_").Gravatar Hugo Herbelin2017-10-05
* | Efficient computation of the names contained in an environment.Gravatar Pierre-Marie Pédrot2017-09-28
* | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
|/
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Deprecate options that were introduced for compatibility with 8.4.Gravatar Guillaume Melquiond2017-06-14
* Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
* [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
* Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
* Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Reordering Termops w.r.t. Evd and Namegen in engine folder.Gravatar Pierre-Marie Pédrot2016-10-30
* CLEANUP: Namegen.to_avoidGravatar Matej Kosik2016-10-20
* CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Gravatar Matej Kosik2016-10-19
* CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-08-17
|\
| * Fixing printing in debugger (no global env in debugger).Gravatar Hugo Herbelin2016-08-17
* | CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-11
* | CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-11
|/
* Better algorithm for variable deambiguation in term printing.Gravatar Pierre-Marie Pédrot2016-06-23
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-18
* Adding a new folder corresponding to the low-level part of the pretyperGravatar Pierre-Marie Pédrot2015-02-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 04:41:32 +0000