aboutsummaryrefslogtreecommitdiff
path: root/proofs/goal.ml
AgeCommit message (Expand)Author
2020-08-26Make future_goals stack explicit in the evarmapMaxime Dénès
2020-08-26Better encapsulation of future goalsMaxime Dénès
2020-08-06Actually use the default instance stored inside named_context_val.Pierre-Marie Pédrot
2020-08-06Use the evarinfo-stored identity substitution where applicable.Pierre-Marie Pédrot
2020-08-06Store the default evar instance inside the evar info.Pierre-Marie Pédrot
2020-07-08Remove Evarutil.new_pure_evar_full from the API.Pierre-Marie Pédrot
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
2020-03-30Merge PR #11817: [cleanup] Remove unnecessary Map/Set module creationGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-13[cleanup] Remove unnecessary Map/Set module creationEmilio Jesus Gallego Arias
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-08-29Solve universe error with SSR 'rewrite !term'Andreas Lynge
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-03-25Fix #9652: rewrite fails to detect lack of progressGaëtan Gilbert
2019-02-08Fix indentation (removing tabs)Matthieu Sozeau
2019-02-08Evd/evarsolve: add an abstraction field to evars for unificationMatthieu Sozeau
2018-10-30Avoid passing dummy env to error printerMaxime Dénès
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-09-17Ensure_prev_proof returns a proof that has underlying differences fromJim Fehrle
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-03-27Congruence: getting rid of a detour by the compatibility layer of proof engine.Hugo Herbelin
2018-03-08Proof engine: using save_future_goal when relevant.Hugo Herbelin
2018-03-08Proof engine: consider the pair principal and future goals as an entity.Hugo Herbelin
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-04Finish removing Show Goal uidGaëtan Gilbert
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Funind API using EConstr.Pierre-Marie Pédrot
2017-02-14Refine API using EConstr.Pierre-Marie Pédrot
2017-02-14Goal API using EConstr.Pierre-Marie Pédrot
2017-02-14Unification API using EConstr.Pierre-Marie Pédrot
2016-08-30CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Matej Kosik
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Monotonizing the Evarutil module.Pierre-Marie Pédrot
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-04Occur-check in refine.Arnaud Spiwack
2014-10-16Put evars remaining after a tactic on the shelf.Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:07:41 +0000