aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/detyping.ml
Commit message (Expand)AuthorAge
* Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
* Change the proj_ind field from MutInd.t to inductive.Gravatar Pierre-Marie Pédrot2018-06-23
* Merge PR #7797: Remove reference name type.Gravatar Enrico Tassi2018-06-19
|\
| * Remove reference name type.Gravatar Maxime Dénès2018-06-18
* | Remove the proj_body field from the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
|/
* [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
* Remove some occurrences of Evd.emptyGravatar Maxime Dénès2018-05-25
* Moving Option.smart_map to Option.Smart.map.Gravatar Hugo Herbelin2018-05-23
* Collecting List.smart_* functions into a module List.Smart.Gravatar Hugo Herbelin2018-05-23
* Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
* Always print explanation for univ inconsistency, rm Flags.univ_printGravatar Gaëtan Gilbert2018-04-26
* Detyping: Adding a variant of share_names for patterns.Gravatar Hugo Herbelin2018-03-28
* Detyping: Making detype_fix/detype_cofix polymorphic combinator (step 1).Gravatar Hugo Herbelin2018-03-28
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 22:05:32 +0000