aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typing.ml
Commit message (Expand)AuthorAge
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
* [econstr] Forbid calling `to_constr` in open terms.Gravatar Emilio Jesus Gallego Arias2018-03-31
* Adding a missing unification in typing.ml.Gravatar Hugo Herbelin2018-03-09
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Hugo Herbelin2018-02-20
* Define EConstr version of [push_rec_types].Gravatar Cyprien Mangin2018-01-19
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| * Update various comments to use "template polymorphism"Gravatar Gaetan Gilbert2017-04-11
|/
* 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
* Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
* Clenv 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
* Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Evarsolve API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Evardefine API using EConstr.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
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-14
|/|
| * Fixing #5077 (failure on typing a fixpoint with evars in its type).Gravatar Hugo Herbelin2016-09-10
* | Make it a bit more obvious when variables are of type unit.Gravatar Guillaume Melquiond2016-08-10
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* | Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* | Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
| * | Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | | Splitting Evarutil in two distinct files.Gravatar Pierre-Marie Pédrot2016-03-20
* | | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \ \
* | | | Renaming functions in Typing to stick to the standard e_* scheme.Gravatar Pierre-Marie Pédrot2016-02-15
| * | | 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
* | | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2015-12-31
|\| |
| * | (Partial) fix for bug #4453: raise an error instead of an anomaly.Gravatar Matthieu Sozeau2015-12-17
* | | Fixing unexpected length of context in a typing function, detected byGravatar Hugo Herbelin2015-12-15