aboutsummaryrefslogtreecommitdiff
path: root/engine/termops.ml
AgeCommit message (Expand)Author
2019-05-13Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.Hugo Herbelin
2019-05-13Moving Evd.evars_of_term from constr to econstr + consequences.Hugo Herbelin
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-02-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
2019-02-04Merge PR #6914: Primitive integersPierre-Marie Pédrot
2019-02-04Primitive integersMaxime Dénès
2019-01-06Renaming pr_evar_suggested_name into -> evar_suggested_name.Hugo Herbelin
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-16Termops.iter_constr_with_full_binders = EConstr.iter_with_full_bindersGaëtan Gilbert
2018-11-16Fix lifting in foo_with_full_binders for (co)fixpointsGaëtan Gilbert
2018-11-06Move debug term printer to kernelMaxime Dénès
2018-11-05Merge PR #8842: Towards seeing Global purely as a wrapper on top of kernel fu...Maxime Dénès
2018-11-03Merge PR #8852: Use the obligation evar flagPierre-Marie Pédrot
2018-10-31Renaming is_template_polymorphic -> is_template_polymorphic_ind.Hugo Herbelin
2018-10-30Generalizing the various evar_map printers in Termops over an environment.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:36:34 +0000