aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretyping.ml
AgeCommit message (Expand)Author
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
2017-11-28Merge PR #1033: Universe binder improvementsMaxime Dénès
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
2017-11-25Fix interpretation of global universes in univdecl constraints.Gaëtan Gilbert
2017-11-24Use Maps and ids for universe bindersGaëtan Gilbert
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-11-08Merge PR #922: New beta-iota compatibility refinementsMaxime Dénès
2017-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
2017-09-15Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.Maxime Dénès
2017-09-12Port is_Set and is_Type to EConstr, as was is_Prop already.Guillaume Melquiond
2017-09-08Parse directly to Sorts.family when appropriate.Gaëtan Gilbert
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-08-21Fixing another regression with 8.4 wrt to βι-normalization of created hyps.Hugo Herbelin
2017-08-01Remove understand_tcc_evars.Maxime Dénès
2017-08-01Move type_uconstr to Tacinterp.Maxime Dénès
2017-08-01Remove understand_judgment and understand_judgment_tcc.Maxime Dénès
2017-08-01Remove allow_anonymous_refs.Maxime Dénès
2017-08-01Remove pure_open_constr (now open_constr)Maxime Dénès
2017-08-01Move glob_constr_ltac_closure to evar_refiner.Maxime Dénès
2017-07-29closing bug 5315Julien Forest
2017-07-13Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-09A fix to #5414 (ident bound by ltac names now known for "match").Hugo Herbelin
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-06Merge PR#716: Don't double up on periods in anomaliesMaxime Dénès
2017-06-05Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...Maxime Dénès
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-31Using a more explicit algebraic type for evars of kind "MatchingVar".Hugo Herbelin
2017-05-30Support for using type information to infer more precise evar sources.Hugo Herbelin
2017-05-25Merge PR#608: Allow Ltac2 as a pluginMaxime Dénès
2017-05-25Merge PR#481: [option] Remove support for non-synchronous options.Maxime Dénès
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-05-19Merge branch 'master' into ltac2-hooksPierre-Marie Pédrot
2017-05-03Generalizing the tactic-in-term embedding to any generic argument.Pierre-Marie Pédrot
2017-05-03Type@{_} should not produce a flexible algebraic universe.Gaetan Gilbert
2017-05-03Allow flexible anonymous universes in instances and sorts.Gaetan Gilbert
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-27Fix omitted labels in function callsGaetan Gilbert
2017-04-25[location] [ast] Port module AST to CAstEmilio Jesus Gallego Arias
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-24[location] Switch glob_constr to Loc.locatedEmilio Jesus Gallego Arias
2017-04-11Merge PR#543: Sanitize instance interpretationMaxime Dénès
2017-04-07Merge branch 'master' into econstrPierre-Marie Pédrot
2017-04-06Merge PR#508: Optimize pending evarsMaxime Dénès
2017-04-06Factor interp_instance out of Pretyping.pretype_globalGaetan Gilbert
2017-04-06Avoid strange shadowing of Pretyping.interp_universe_level_nameGaetan Gilbert
2017-04-04Merge branch 'trunk' into pr379Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 05:36:20 +0000