aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
Commit message (Expand)AuthorAge
* Change QuestionMark for better record field missing error message.Gravatar Siddharth Bhat2018-07-17
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* Stronger invariants in unification signature.Gravatar Pierre-Marie Pédrot2018-06-04
* [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
* Collecting List.smart_* functions into a module List.Smart.Gravatar Hugo Herbelin2018-05-23
* Merge PR #7384: Split UniversesGravatar Pierre-Marie Pédrot2018-05-22
|\
* \ Merge PR #6965: [api] Move universe syntax to `Glob_term`Gravatar Pierre-Marie Pédrot2018-05-18
|\ \
| | * Make set minimization option internal to UniversesGravatar Gaëtan Gilbert2018-05-17
| |/ |/|
* | Deprecate Evarconv.e_conv,e_cumulGravatar Gaëtan Gilbert2018-05-11
| * [api] Move universe syntax to `Glob_term`Gravatar Emilio Jesus Gallego Arias2018-05-08
|/
* Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.Gravatar Hugo Herbelin2018-04-26
* 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
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* \ Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \
| * | Remove VOld compatibility flag.Gravatar Théo Zimmermann2018-03-02
* | | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
|/ /
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)Gravatar Enrico Tassi2018-02-19
* Merge PR #6651: Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-02-12
|\
| * Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-01-30
* | Cleanup name-binding structure for fresh evar name generation.Gravatar Pierre-Marie Pédrot2018-01-02
|/
* Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
* Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\
* | [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
| * Fix interpretation of global universes in univdecl constraints.Gravatar Gaëtan Gilbert2017-11-25
| * Use Maps and ids for universe bindersGravatar Gaëtan Gilbert2017-11-24
|/
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
* Merge PR #922: New beta-iota compatibility refinementsGravatar Maxime Dénès2017-11-08
|\
* | [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
* | [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
* | Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Maxime Dénès2017-09-15
|\ \
| * | Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Guillaume Melquiond2017-09-12
* | | Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
|/ /
* | Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
| * Fixing another regression with 8.4 wrt to βι-normalization of created hyps.Gravatar Hugo Herbelin2017-08-21
* | Remove understand_tcc_evars.Gravatar Maxime Dénès2017-08-01
* | Move type_uconstr to Tacinterp.Gravatar Maxime Dénès2017-08-01
* | Remove understand_judgment and understand_judgment_tcc.Gravatar Maxime Dénès2017-08-01
* | Remove allow_anonymous_refs.Gravatar Maxime Dénès2017-08-01
* | Remove pure_open_constr (now open_constr)Gravatar Maxime Dénès2017-08-01
* | Move glob_constr_ltac_closure to evar_refiner.Gravatar Maxime Dénès2017-08-01
|/
* closing bug 5315Gravatar Julien Forest2017-07-29
* Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Gravatar Pierre-Marie Pédrot2017-07-13
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Merge PR#716: Don't double up on periods in anomaliesGravatar Maxime Dénès2017-06-06
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 17:23:27 +0000