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