aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.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
* [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
|\
* \ Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...Gravatar Maxime Dénès2017-06-05
|\ \
| | * Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| |/ |/|
| * Using a more explicit algebraic type for evars of kind "MatchingVar".Gravatar Hugo Herbelin2017-05-31
* | Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
|/
* Merge PR#608: Allow Ltac2 as a pluginGravatar Maxime Dénès2017-05-25
|\
* \ 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 branch 'master' into ltac2-hooksGravatar Pierre-Marie Pédrot2017-05-19
| | |\ | | |/ | |/|
| | * Generalizing the tactic-in-term embedding to any generic argument.Gravatar Pierre-Marie Pédrot2017-05-03
| * | Type@{_} should not produce a flexible algebraic universe.Gravatar Gaetan Gilbert2017-05-03
| * | Allow flexible anonymous universes in instances and sorts.Gravatar Gaetan Gilbert2017-05-03
| |/
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 12:15:38 +0000