aboutsummaryrefslogtreecommitdiff
path: root/proofs/goal.ml
AgeCommit message (Expand)Author
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
2014-09-12Use evar name to print goal.Hugo Herbelin
2014-09-04Only using filtered hyps in Goal.enter.Pierre-Marie Pédrot
2014-09-04Ensuring the invariant that hypotheses and named context of the environment ofPierre-Marie Pédrot
2014-09-04Fix: shelve_unifiable did not work modulo evar instantiation.Arnaud Spiwack
2014-09-03Putting back normalized goals when entering them.Pierre-Marie Pédrot
2014-08-21Removing unused parts of the Goal.sensitive monad.Pierre-Marie Pédrot
2014-08-19Removing a use of Goal.refine.Pierre-Marie Pédrot
2014-08-05Goal: API to get the solution of a goalEnrico Tassi
2014-06-17Tentative optimization not to nf_evar too often in the compatibilityPierre-Marie Pédrot
2014-04-23Better representation of evar filters: we represent the vacuous filters ofPierre-Marie Pédrot
2014-03-19Adding phantom types to discriminate normalized goals, and adding a way toPierre-Marie Pédrot
2014-03-07Potentially unused computation in Goal.Pierre-Marie Pédrot
2014-02-27Code refactoring thanks to the new Monad module.Arnaud Spiwack
2014-02-12TC: honor the use_typeclasses flag in pretypingEnrico Tassi
2014-01-10Useless Array.of_listPierre-Marie Pédrot
2014-01-10Exporting the full pretyper options in Goal.constr_of_raw.Pierre-Marie Pédrot
2013-11-30Fixing ltac constr variable handling in refine.Pierre-Marie Pédrot
2013-11-12Useless computation in Goal handle augmentation.ppedrot
2013-11-09Partial applications in Goal.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 01:35:48 +0000