aboutsummaryrefslogtreecommitdiff
path: root/engine/evarutil.ml
AgeCommit message (Expand)Author
2017-12-22Merge PR #6222: Share computation of unifiable evarsMaxime Dénès
2017-12-09[summary] Adapt STM to the new Summary API.Emilio Jesus Gallego Arias
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
2017-11-21[api] Miscellaneous consolidation + moves to engine.Emilio Jesus Gallego Arias
2017-11-21Experimenting with a fine-grained cache for undefined evars in evinfos.Pierre-Marie Pédrot
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
2017-09-27Moving setting of "cleared" evar flag directly in Evd.restrict.Hugo Herbelin
2017-08-29Merge PR #830: Moving assert (the "Cut" rule) to new proof engineMaxime Dénès
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-25Adding intermediate entry point to create an evar in empty rel_context.Hugo Herbelin
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-30Support for using type information to infer more precise evar sources.Hugo Herbelin
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-02Merge PR#582: Fix warningsMaxime Dénès
2017-05-01More consistent writing of de Bruijn.Théo Zimmermann
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-02-14Moving evar-normalization functions to EConstr.Pierre-Marie Pédrot
2017-02-14Namegen primitives now apply on evar constrs.Pierre-Marie Pédrot
2017-02-14Making Evd independent from Namegen.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Evar-normalizing functions now act on EConstrs.Pierre-Marie Pédrot
2017-02-14Removing some return type compatibility layers in Termops.Pierre-Marie Pédrot
2017-02-14Proofview.Goal primitive now return EConstrs.Pierre-Marie Pédrot
2017-02-14Rewrite API using EConstr.Pierre-Marie Pédrot
2017-02-14Hints API using EConstr.Pierre-Marie Pédrot
2017-02-14Leminv API using EConstr.Pierre-Marie Pédrot
2017-02-14Equality API using EConstr.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Refine API using EConstr.Pierre-Marie Pédrot
2017-02-14Making judgment type generic over the type of inner constrs.Pierre-Marie Pédrot
2017-02-14Pretyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarconv API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-10-24Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-21Merge remote-tracking branch 'gforge/v8.5' into v8.6Matthieu Sozeau
2016-09-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-05Fast path in push_rel_context_to_named_context.Pierre-Marie Pédrot
2016-09-02Fast path in whd_evar.Pierre-Marie Pédrot
2016-08-26Removing calls of "Context.Rel.Declaration.to_tuple" functionMatej Kosik
2016-08-26CLEANUP: minor readability improvementsMatej Kosik
2016-08-25CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Matej Kosik
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-08-06Using a dedicated kind of substitutions in evar name generation.Pierre-Marie Pédrot
2016-08-05Using the extended contexts in pretyping.Pierre-Marie Pédrot
2016-08-04Use sets instead of lists for names to avoid in evar generation.Pierre-Marie Pédrot
2016-08-04Simplifying code in evar generation.Pierre-Marie Pédrot
2016-08-04Exporting the renaming API for evar declaration.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:46:46 +0000