aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/detyping.ml
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* detype_case predicate is not optionalGravatar Gaëtan Gilbert2018-02-14
* Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-01-30
* Decompiling pattern-matching: mini-removal dead code.Gravatar Hugo Herbelin2017-12-12
* In printing, factorizing "match" clauses with same right-hand side.Gravatar Hugo Herbelin2017-12-12
* Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
* Merge PR #1084: After testing it in live, writing metas using an ?INTERNAL#42...Gravatar Maxime Dénès2017-10-03
|\
* | 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
| * After testing it in live, writing metas using an ?INTERNAL#42 style is ugly.Gravatar Hugo Herbelin2017-09-23
|/
* Proposing meta names more distinguishable from evar names than ?M42.Gravatar Hugo Herbelin2017-09-21
* A possible fix to BZ#5750 (ability to print context of ltac subterm match).Gravatar Hugo Herbelin2017-09-21
* Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
* Prevent overallocation in Array.map_to_list and remove custom implementation ...Gravatar Guillaume Melquiond2017-08-22
* Merge PR #913: Less allocations in DetypingGravatar Maxime Dénès2017-08-01
|\
* | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| * Add a comment regarding the specialization of the combinator in Detyping.Gravatar Pierre-Marie Pédrot2017-07-26
| * Allocation-friendly detyping of term arrays.Gravatar Pierre-Marie Pédrot2017-07-21
|/
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* 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 PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\
* \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| | * [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| |/
| * Merge PR#544: Anonymous universesGravatar Maxime Dénès2017-05-05
| |\
| | * Allow flexible anonymous universes in instances and sorts.Gravatar Gaetan Gilbert2017-05-03
| * | applied the patch for printing types of let bindings by @herbelinGravatar Abhishek Anand (@brixpro-home)2017-05-02
| |/
| * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* | [location] [ast] Port module AST to CAstGravatar 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] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
* | [location] Move Glob_term.predicate_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | [location] Move Glob_term.cases_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
|/
* Merge PR#379: Introducing evar-insensitive constrsGravatar Maxime Dénès2017-04-11
|\
* | Turning the printing primitive projection parameter flag off by default.Gravatar Hugo Herbelin2017-04-07
* | Turning the printing primitive projection compatibility flag off by default.Gravatar Hugo Herbelin2017-04-07
| * Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
| |\ | |/ |/|
| * Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
| * Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
* | Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| * Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| * Moving printing code from Evd to Termops.Gravatar Pierre-Marie Pédrot2017-02-14
| * Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
| * Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
| * Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
| * Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 00:00:00 +0000