aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typing.ml
Commit message (Expand)AuthorAge
* Remove unused env argument to fresh_sort_in_familyGravatar Gaëtan Gilbert2018-07-03
* Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
* Merge PR #664: Fixing #5500 (missing test in return clause of match leading t...Gravatar Matthieu Sozeau2018-06-14
|\
* | [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
* | Unify pre_env and envGravatar Maxime Dénès2018-05-28
* | Typing implementation doesn't use evdref.Gravatar Gaëtan Gilbert2018-05-14
* | Typing: define functional alternatives to e_* functionsGravatar Gaëtan Gilbert2018-05-14
* | set_solve_evars doesn't use an evar_map refGravatar Gaëtan Gilbert2018-05-11
* | Deprecate Evarconv.e_conv,e_cumulGravatar Gaëtan Gilbert2018-05-11
* | 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
| * Fixing #5500 (missing test in return clause of match leading to anomaly).Gravatar Hugo Herbelin2018-03-27
|/
* 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
|\ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 21:39:30 +0000