aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
Commit message (Expand)AuthorAge
* 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
* 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
|\| |
* | | Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
| * | Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| | * Make the computation of frozen evars lazy in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| | * Fast path in computation of frozen evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| | * Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| |/
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\|
* | 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
* | Cleaning up interfaces.Gravatar Pierre-Marie Pédrot2017-02-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 04:49:24 +0000