aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretyping.ml
AgeCommit message (Expand)Author
2018-09-10Files pretyping.ml, glob_obs.ml, evarutil.ml: rewording/typos in some comments.Hugo Herbelin
2018-08-17More efficient computation of avoided variables during pretyping.Pierre-Marie Pédrot
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
2018-06-18Remove reference name type.Maxime Dénès
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-06-04Stronger invariants in unification signature.Pierre-Marie Pédrot
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-05-22Merge PR #7384: Split UniversesPierre-Marie Pédrot
2018-05-18Merge PR #6965: [api] Move universe syntax to `Glob_term`Pierre-Marie Pédrot
2018-05-17Make set minimization option internal to UniversesGaëtan Gilbert
2018-05-11Deprecate Evarconv.e_conv,e_cumulGaëtan Gilbert
2018-05-08[api] Move universe syntax to `Glob_term`Emilio Jesus Gallego Arias
2018-04-26Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.Hugo Herbelin
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-03-31[econstr] Forbid calling `to_constr` in open terms.Emilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-02Remove VOld compatibility flag.Théo Zimmermann
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-19pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)Enrico Tassi
2018-02-12Merge PR #6651: Use r.(p) syntax to print primitive projections.Maxime Dénès
2018-01-30Use r.(p) syntax to print primitive projections.Maxime Dénès
2018-01-02Cleanup name-binding structure for fresh evar name generation.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:16:18 +0000