aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2014-11-23One more word about "simpl f": avoid "simpl f" to be printed "simpl f",Hugo Herbelin
2014-11-22Removing useless flag of the historical move tactic.Pierre-Marie Pédrot
2014-11-22Exporting a primitive allowing to run completely the tactic monad.Pierre-Marie Pédrot
2014-11-20Exporting the function handling side-effects only applied to terms.Pierre-Marie Pédrot
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-09new: Optimize Proof, Optimize HeapEnrico Tassi
2014-11-08Follow up to experimental eager evar unification in bcba6d1bc9:Hugo Herbelin
2014-11-07Removing the legacy intro tactic code.Pierre-Marie Pédrot
2014-11-04Removing the old rename tactic.Pierre-Marie Pédrot
2014-11-02Plural and singular forms in error messages.Hugo Herbelin
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-01Info: dispatching-branches are declared as such in the info trace.Arnaud Spiwack
2014-11-01Add [Info] command.Arnaud Spiwack
2014-11-01An API for info traces.Arnaud Spiwack
2014-10-27Cleaning and documenting Clenv.make_evar_clausePierre-Marie Pédrot
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-25VarInstance are also goals.Hugo Herbelin
2014-10-24Change reduction_of_red_expr to return an e_reduction_function returningMatthieu Sozeau
2014-10-23Monad: change the error managing of two-list combinators.Arnaud Spiwack
2014-10-23Evd.future_goals: forgot to revert the list in two places.Arnaud Spiwack
2014-10-23Proofview: forgot to change an exception after refactoring in ( 9f51aafebd5f3...Arnaud Spiwack
2014-10-22Specializing tclBREAK so that it can choose the return exception in casePierre-Marie Pédrot
2014-10-22Oversight in ce260a0db279ce09dda70e079ae3c35b49f05ec4 (Proper scoping of futu...Arnaud Spiwack
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: remove and inline [on_advance] function.Arnaud Spiwack
2014-10-22Proofview: add a lens for the evar_map and factor some code.Arnaud Spiwack
2014-10-22Proofview: use an iter-like combinator rather than a fold_left-like one for d...Arnaud Spiwack
2014-10-22Add more primitives to the [Monad.Make] arguments.Arnaud Spiwack
2014-10-22Improve readability the "lenses" in Proofview, using interfaces.Arnaud Spiwack
2014-10-22Proofview: clean up code a little.Arnaud Spiwack
2014-10-22Proofview: move [list_goto] to the [CList] module.Arnaud Spiwack
2014-10-22Proofview: replace the functions iter_list and iter_list2 by generic monadic ...Arnaud Spiwack
2014-10-22Proofview: clean up commented out code.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-22Proofview: factor init and dependent_init.Arnaud Spiwack
2014-10-22Remove unused functions for side effects.Arnaud Spiwack
2014-10-22Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Arnaud Spiwack
2014-10-21Lazily check that an argument is dependent when constructing evar clauses.Pierre-Marie Pédrot
2014-10-21Adding an evar version of the make_clenv function.Pierre-Marie Pédrot
2014-10-16Revert "Naming main goal "Main""Hugo Herbelin
2014-10-16Refactoring proofview: make the definition of the logic monad polymorphic.Arnaud Spiwack
2014-10-16Grab Existential Variables: restore the goal order from v8.4.Arnaud Spiwack
2014-10-16Proofview: cleanup: no more reference to Goal.goal.Arnaud Spiwack
2014-10-16Put evars remaining after a tactic on the shelf.Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 07:40:14 +0000