aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
Commit message (Expand)AuthorAge
* 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
| |/
| * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| * Fix omitted labels in function callsGravatar 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
|/
* Merge PR#543: Sanitize instance interpretationGravatar Maxime Dénès2017-04-11
|\
* \ Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\ \
| * \ Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
| |\ \
| | | * Factor interp_instance out of Pretyping.pretype_globalGravatar Gaetan Gilbert2017-04-06
| | | * Avoid strange shadowing of Pretyping.interp_universe_level_nameGravatar Gaetan Gilbert2017-04-06
| | |/ | |/|
* | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 13:48:17 +0000