aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/detyping.ml
Commit message (Expand)AuthorAge
* 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
| * Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Cleaning up opening of the EConstr module in pretyping folder.Gravatar Pierre-Marie Pédrot2017-02-14
| * Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|/
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Two protections against failures when printing evar_map.Gravatar Hugo Herbelin2016-08-17
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\
* \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|\ \
| * | Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
| | * CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| |/ |/|
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\|
| * Add an option to deactivate compatibility printing of primitiveGravatar Matthieu Sozeau2015-12-02
* | Experimenting printing the type of the defined term of a LetIn whenGravatar Hugo Herbelin2015-11-07
|/
* Using "__" rather than this unelegant arbitrary "A" for the name of variables...Gravatar Hugo Herbelin2015-10-18
* Using appropriate lambda decomposition function counting let-ins whenGravatar Hugo Herbelin2015-10-18
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07