aboutsummaryrefslogtreecommitdiff
path: root/engine/termops.ml
AgeCommit message (Expand)Author
2018-10-30Switch to using the obligation_evar flag instead of the evar sourceMatthieu Sozeau
2018-10-26[typeclasses] functionalize typeclass evar handlingMatthieu Sozeau
2018-10-26Cleanup evar_extra: remove evar_info's store and add maps to evar_mapMatthieu Sozeau
2018-10-26Merge PR #7186: Moving `fold_constr_with_full_binders` to a placeMaxime Dénès
2018-10-16Simplify vars_of_global usageGaëtan Gilbert
2018-10-14A useless occurrence of Global.env.Hugo Herbelin
2018-10-12Moving local copy fold_constr_with_full_binders in assumptions.ml to constr.ml.Hugo Herbelin
2018-09-26[print] Restrict use of "debug" Termops printer.Emilio Jesus Gallego Arias
2018-09-23Checking if low-level name printers are used on purpose or not.Hugo Herbelin
2018-09-03Adding combinators preserving expanded form of branches and pred. of "match".Hugo Herbelin
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-18Remove reference name type.Maxime Dénès
2018-06-04[termops] Update type of function, anyways not used in the codebase.Emilio Jesus Gallego Arias
2018-06-04Merge PR #7216: Replace uses of Termops.dependent by more specific functions.Matthieu Sozeau
2018-05-30[api] Remove deprecated objects in engine / interp / libraryEmilio Jesus Gallego Arias
2018-05-28Merge PR #7521: Fix soundness bug with VM/native and cofixpointsPierre-Marie Pédrot
2018-05-28Unify pre_env and envMaxime Dénès
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-23Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.Hugo Herbelin
2018-05-17Split off Universes functions about substitutions and constraintsGaëtan Gilbert
2018-05-17Split off Universes functions dealing with names.Gaëtan Gilbert
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-04-10Replace uses of Termops.dependent by more specific functions.Pierre-Marie Pédrot
2018-03-24Slightly refining some error messages about unresolvable evars.Hugo Herbelin
2018-03-09Delayed weak constraints for cumulative inductive types.Gaëtan Gilbert
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-03-06Deprecate UState aliases in Evd.Gaëtan Gilbert
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
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-01-17Use let-in aware prod_applist_assum in dtauto and firstorder.Jasper Hugunin
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-11-05Cosmetic changes in evar_map printer.Hugo Herbelin
2017-11-05Preventively protect locally against failures of evar_map printer.Hugo Herbelin
2017-09-28Efficient computation of the names contained in an environment.Pierre-Marie Pédrot
2017-09-12Port is_Set and is_Type to EConstr, as was is_Prop already.Guillaume Melquiond
2017-08-01Merge PR #913: Less allocations in DetypingMaxime Dénès
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-21No useless reallocation in Termops.collapse_appl.Pierre-Marie Pédrot
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-16Squashed commit of the following:Amin Timany
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-06-01Merge PR#561: Improving the Name APIMaxime Dénès
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:21:17 +0000