aboutsummaryrefslogtreecommitdiff
path: root/engine/namegen.ml
AgeCommit message (Expand)Author
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-03-08Merge PR #6899: [compat] Remove "Standard Proposition Elimination"Maxime Dénès
2018-03-08Merge PR #6582: Mangle auto-generated namesMaxime Dénès
2018-03-03[compat] Remove "Standard Proposition Elimination"Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-17Implement name mangling optionJasper Hugunin
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-11-05Fixing a cause of failure of evar_map printer in debugger.Hugo Herbelin
2017-10-28Fixing #5401 (printing of patterns with bound anonymous variables).Hugo Herbelin
2017-10-06Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type "_som...Maxime Dénès
2017-10-05Fixing BZ#5769 (variable of type "_something" was named after invalid "_").Hugo Herbelin
2017-09-28Efficient computation of the names contained in an environment.Pierre-Marie Pédrot
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-14Deprecate options that were introduced for compatibility with 8.4.Guillaume Melquiond
2017-06-14Remove support for Coq 8.4.Guillaume Melquiond
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-04-01Actually exporting delayed universes in the EConstr implementation.Pierre-Marie Pédrot
2017-02-14Namegen primitives now apply on evar constrs.Pierre-Marie Pédrot
2016-10-30Reordering Termops w.r.t. Evd and Namegen in engine folder.Pierre-Marie Pédrot
2016-10-20CLEANUP: Namegen.to_avoidMatej Kosik
2016-10-19CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Matej Kosik
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-08-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-08-17Fixing printing in debugger (no global env in debugger).Hugo Herbelin
2016-08-11CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" functionMatej Kosik
2016-08-11CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" functionMatej Kosik
2016-06-23Better algorithm for variable deambiguation in term printing.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-18Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-27Adding a new folder corresponding to the low-level part of the pretyperPierre-Marie Pédrot