aboutsummaryrefslogtreecommitdiff
path: root/proofs/proofview.mli
AgeCommit message (Expand)Author
2016-03-20Moving Proofview to pretyping/.Pierre-Marie Pédrot
2016-03-20Moving Refine to its proper module.Pierre-Marie Pédrot
2016-03-20Making Proofview independent of Logic.Pierre-Marie Pédrot
2016-03-20Extruding the code for the Existential command from Proofview.Pierre-Marie Pédrot
2016-03-14Fix the comment of Refine.refineMatthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2016-01-02Use streams rather than strings to handle bullet suggestions.Guillaume Melquiond
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-09Adding an unshelve tactical.Pierre-Marie Pédrot
2015-10-29Removing the evar_map argument from s_enter.Pierre-Marie Pédrot
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-20Proofview.Goal.sigma returns an indexed evarmap.Pierre-Marie Pédrot
2015-10-20Indexing Proofview.goals with a stage.Pierre-Marie Pédrot
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-10-20Renaming Goal.enter field into s_enter.Pierre-Marie Pédrot
2015-10-19Adding a monotonic variant of Goal.enter and Goal.nf_enter.Pierre-Marie Pédrot
2015-10-18Constraining refine to monotonic functions.Pierre-Marie Pédrot
2015-05-06Exposing the minimal amount of internal of the Logic monad in order toPierre-Marie Pédrot
2015-02-23Fix some typos in comments.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2015-01-08Fixed and extend bullet related info/error messages. + doc.Pierre Courtieu
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-12Make sure the goals on the shelve are identified as goal and unresolvable for...Arnaud Spiwack
2014-12-07Exporting store of goals so that new_evar in convert, intro, etc. canHugo Herbelin
2014-11-30Adding missing unsafe primitives to Proofview.Pierre-Marie Pédrot
2014-11-09new: Optimize Proof, Optimize HeapEnrico Tassi
2014-11-01Info: do not record info trace unless needed.Arnaud Spiwack
2014-11-01Info: print a name for the primitive tactics in [Proofview].Arnaud Spiwack
2014-11-01Add [Info] command.Arnaud Spiwack
2014-11-01An API for info traces.Arnaud Spiwack
2014-10-22Specializing tclBREAK so that it can choose the return exception in casePierre-Marie Pédrot
2014-10-22Proofview: documentation and re-ordering.Arnaud Spiwack
2014-10-22Split [Proofview] into a file where the basic operations on the state are def...Arnaud Spiwack
2014-10-22Make names in [Proofview_monad] more uniform.Arnaud Spiwack
2014-10-22Proofview: move [list_goto] to the [CList] module.Arnaud Spiwack
2014-10-22Proofview: remove a redundant primitive.Arnaud Spiwack
2014-10-22Proofview: move more functions to the Unsafe module.Arnaud Spiwack
2014-10-22Proofview: split [V82] module into [Unsafe] and [V82].Arnaud Spiwack
2014-10-22Proofview.mli: no more reference to Goal.goal.Arnaud Spiwack
2014-10-22Remove unused functions for side effects.Arnaud Spiwack
2014-10-16Refactoring proofview: make the definition of the logic monad polymorphic.Arnaud Spiwack
2014-10-16Put evars remaining after a tactic on the shelf.Arnaud Spiwack
2014-10-16Proofview: remove unused [refresh_sigma] compatibility primitive.Arnaud Spiwack
2014-10-16Expose Proofview.Refine.with_type in the API.Arnaud Spiwack
2014-10-16Proofview.Refine: remove the handle type, and simplify the API.Arnaud Spiwack
2014-10-13Adding a tactic which fails if one of the goals under focus is dependent in a...Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:57:31 +0000