index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
Commit message (
Expand
)
Author
Age
...
*
VarInstance are also goals.
Hugo Herbelin
2014-10-25
*
Change reduction_of_red_expr to return an e_reduction_function returning
Matthieu Sozeau
2014-10-24
*
Monad: change the error managing of two-list combinators.
Arnaud Spiwack
2014-10-23
*
Evd.future_goals: forgot to revert the list in two places.
Arnaud Spiwack
2014-10-23
*
Proofview: forgot to change an exception after refactoring in ( 9f51aafebd5f3...
Arnaud Spiwack
2014-10-23
*
Specializing tclBREAK so that it can choose the return exception in case
Pierre-Marie Pédrot
2014-10-22
*
Oversight in ce260a0db279ce09dda70e079ae3c35b49f05ec4 (Proper scoping of futu...
Arnaud Spiwack
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: remove and inline [on_advance] function.
Arnaud Spiwack
2014-10-22
*
Proofview: add a lens for the evar_map and factor some code.
Arnaud Spiwack
2014-10-22
*
Proofview: use an iter-like combinator rather than a fold_left-like one for d...
Arnaud Spiwack
2014-10-22
*
Add more primitives to the [Monad.Make] arguments.
Arnaud Spiwack
2014-10-22
*
Improve readability the "lenses" in Proofview, using interfaces.
Arnaud Spiwack
2014-10-22
*
Proofview: clean up code a little.
Arnaud Spiwack
2014-10-22
*
Proofview: move [list_goto] to the [CList] module.
Arnaud Spiwack
2014-10-22
*
Proofview: replace the functions iter_list and iter_list2 by generic monadic ...
Arnaud Spiwack
2014-10-22
*
Proofview: clean up commented out code.
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
*
Proofview: factor init and dependent_init.
Arnaud Spiwack
2014-10-22
*
Remove unused functions for side effects.
Arnaud Spiwack
2014-10-22
*
Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.
Arnaud Spiwack
2014-10-22
*
Lazily check that an argument is dependent when constructing evar clauses.
Pierre-Marie Pédrot
2014-10-21
*
Adding an evar version of the make_clenv function.
Pierre-Marie Pédrot
2014-10-21
*
Revert "Naming main goal "Main""
Hugo Herbelin
2014-10-16
*
Refactoring proofview: make the definition of the logic monad polymorphic.
Arnaud Spiwack
2014-10-16
*
Grab Existential Variables: restore the goal order from v8.4.
Arnaud Spiwack
2014-10-16
*
Proofview: cleanup: no more reference to Goal.goal.
Arnaud Spiwack
2014-10-16
*
Put evars remaining after a tactic on the shelf.
Arnaud Spiwack
2014-10-16
*
Refine: proper scoping of the future goals.
Arnaud Spiwack
2014-10-16
*
Goal: remove [advance] from the API.
Arnaud Spiwack
2014-10-16
*
Proofview: remove unused [refresh_sigma] compatibility primitive.
Arnaud Spiwack
2014-10-16
*
Goal: remove some functions from the compatibility layer.
Arnaud Spiwack
2014-10-16
*
Goal: remove most of the API (make [Goal.goal] concrete).
Arnaud Spiwack
2014-10-16
*
Make [Goal.goal] be exactly [Evar.t].
Arnaud Spiwack
2014-10-16
*
Goal: remove dead code.
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
*
Move the handling of the principal evar from refine to evd.
Arnaud Spiwack
2014-10-16
*
Move the handling a new evars from the [Proofview.Refine] module to [Evd].
Arnaud Spiwack
2014-10-16
*
Proofview.Refine: delay the marking of new evars as goals from [new_evar] to ...
Arnaud Spiwack
2014-10-16
*
Proofview: small optimisation/simplification.
Arnaud Spiwack
2014-10-16
*
Add support for deactivating type class inference from induction/destruct.
Hugo Herbelin
2014-10-13
*
Adding a tactic which fails if one of the goals under focus is dependent in a...
Hugo Herbelin
2014-10-13
*
Naming main goal "Main"
Hugo Herbelin
2014-10-13
*
Added support for having one subgoal inheriting the name of its father in Ref...
Hugo Herbelin
2014-10-09
[prev]
[next]