aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofview.ml
Commit message (Expand)AuthorAge
* Plural and singular forms in error messages.Gravatar Hugo Herbelin2014-11-02
* Info: do not record info trace unless needed.Gravatar Arnaud Spiwack2014-11-01
* Info: print a name for the primitive tactics in [Proofview].Gravatar Arnaud Spiwack2014-11-01
* Info: dispatching-branches are declared as such in the info trace.Gravatar Arnaud Spiwack2014-11-01
* Add [Info] command.Gravatar Arnaud Spiwack2014-11-01
* An API for info traces.Gravatar Arnaud Spiwack2014-11-01
* VarInstance are also goals.Gravatar Hugo Herbelin2014-10-25
* Monad: change the error managing of two-list combinators.Gravatar Arnaud Spiwack2014-10-23
* Proofview: forgot to change an exception after refactoring in ( 9f51aafebd5f3...Gravatar Arnaud Spiwack2014-10-23
* Oversight in ce260a0db279ce09dda70e079ae3c35b49f05ec4 (Proper scoping of futu...Gravatar Arnaud Spiwack2014-10-22
* Proofview: documentation and re-ordering.Gravatar Arnaud Spiwack2014-10-22
* Split [Proofview] into a file where the basic operations on the state are def...Gravatar Arnaud Spiwack2014-10-22
* Make names in [Proofview_monad] more uniform.Gravatar Arnaud Spiwack2014-10-22
* Proofview: remove and inline [on_advance] function.Gravatar Arnaud Spiwack2014-10-22
* Proofview: add a lens for the evar_map and factor some code.Gravatar Arnaud Spiwack2014-10-22
* Proofview: use an iter-like combinator rather than a fold_left-like one for d...Gravatar Arnaud Spiwack2014-10-22
* Add more primitives to the [Monad.Make] arguments.Gravatar Arnaud Spiwack2014-10-22
* Improve readability the "lenses" in Proofview, using interfaces.Gravatar Arnaud Spiwack2014-10-22
* Proofview: clean up code a little.Gravatar Arnaud Spiwack2014-10-22
* Proofview: move [list_goto] to the [CList] module.Gravatar Arnaud Spiwack2014-10-22
* Proofview: replace the functions iter_list and iter_list2 by generic monadic ...Gravatar Arnaud Spiwack2014-10-22
* Proofview: clean up commented out code.Gravatar Arnaud Spiwack2014-10-22
* Proofview: remove a redundant primitive.Gravatar Arnaud Spiwack2014-10-22
* Proofview: move more functions to the Unsafe module.Gravatar Arnaud Spiwack2014-10-22
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Proofview: factor init and dependent_init.Gravatar Arnaud Spiwack2014-10-22
* Remove unused functions for side effects.Gravatar Arnaud Spiwack2014-10-22
* Revert "Naming main goal "Main""Gravatar Hugo Herbelin2014-10-16
* Refactoring proofview: make the definition of the logic monad polymorphic.Gravatar Arnaud Spiwack2014-10-16
* Grab Existential Variables: restore the goal order from v8.4.Gravatar Arnaud Spiwack2014-10-16
* Proofview: cleanup: no more reference to Goal.goal.Gravatar Arnaud Spiwack2014-10-16
* Put evars remaining after a tactic on the shelf.Gravatar Arnaud Spiwack2014-10-16
* Refine: proper scoping of the future goals.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove [advance] from the API.Gravatar Arnaud Spiwack2014-10-16
* Proofview: remove unused [refresh_sigma] compatibility primitive.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove some functions from the compatibility layer.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove most of the API (make [Goal.goal] concrete).Gravatar Arnaud Spiwack2014-10-16
* Expose Proofview.Refine.with_type in the API.Gravatar Arnaud Spiwack2014-10-16
* Proofview.Refine: remove the handle type, and simplify the API.Gravatar Arnaud Spiwack2014-10-16
* Move the handling of the principal evar from refine to evd.Gravatar Arnaud Spiwack2014-10-16
* Move the handling a new evars from the [Proofview.Refine] module to [Evd].Gravatar Arnaud Spiwack2014-10-16
* Proofview.Refine: delay the marking of new evars as goals from [new_evar] to ...Gravatar Arnaud Spiwack2014-10-16
* Proofview: small optimisation/simplification.Gravatar Arnaud Spiwack2014-10-16
* Adding a tactic which fails if one of the goals under focus is dependent in a...Gravatar Hugo Herbelin2014-10-13
* Naming main goal "Main"Gravatar Hugo Herbelin2014-10-13
* Added support for having one subgoal inheriting the name of its father in Ref...Gravatar Hugo Herbelin2014-10-09
* A version of convert_concl and convert_hyp in new proof engine.Gravatar Hugo Herbelin2014-10-09
* Make tclEFFECTS also update the env in the proof monadGravatar Enrico Tassi2014-10-06
* A few Global.env removed.Gravatar Hugo Herbelin2014-10-04
* Merging some functions from evarutil.ml/evd.ml.Gravatar Hugo Herbelin2014-09-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-19 00:11:17 +0000