aboutsummaryrefslogtreecommitdiff
path: root/proofs/goal.ml
AgeCommit message (Expand)Author
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
2014-10-16Goal: remove [advance] from the API.Arnaud Spiwack
2014-10-16Goal: remove some functions from the compatibility layer.Arnaud Spiwack
2014-10-16Goal: remove most of the API (make [Goal.goal] concrete).Arnaud Spiwack
2014-10-16Make [Goal.goal] be exactly [Evar.t].Arnaud Spiwack
2014-10-16Goal: remove dead code.Arnaud Spiwack
2014-10-16Proofview.Refine: delay the marking of new evars as goals from [new_evar] to ...Arnaud Spiwack
2014-10-13Adding a tactic which fails if one of the goals under focus is dependent in a...Hugo Herbelin
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-29Merging some functions from evarutil.ml/evd.ml.Hugo Herbelin
2014-09-27Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.Pierre-Marie Pédrot
2014-09-17Fix bug #3593, making constr_eq and progress work up toMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:46:43 +0000