aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Exporting store of goals so that new_evar in convert, intro, etc. canGravatar Hugo Herbelin2014-12-07
* Occur-check in refine.Gravatar Arnaud Spiwack2014-12-04
* Refine primitive: [unsafe] is now true by default.Gravatar Arnaud Spiwack2014-12-04
* Some refactoring following previous commit.Gravatar Arnaud Spiwack2014-12-04
* Better implementation of 4a858a51322f2dd488b02130ca82ebcc4dc9ca35.Gravatar Arnaud Spiwack2014-12-04
* Factoring 2ee213b824dda48c3fe60e95316daf09f07e8075.Gravatar Arnaud Spiwack2014-12-04
* Fixing bug #3682.Gravatar Pierre-Marie Pédrot2014-11-30
* Adding missing unsafe primitives to Proofview.Gravatar Pierre-Marie Pédrot2014-11-30
* Fix (somewhat obsolete) [Existential] command, which conflicted with the shelf.Gravatar Arnaud Spiwack2014-11-28
* Tactic primitives: missing [advance] lead to spurious dangling goals.Gravatar Arnaud Spiwack2014-11-28
* One more word about "simpl f": avoid "simpl f" to be printed "simpl f",Gravatar Hugo Herbelin2014-11-23
* Removing useless flag of the historical move tactic.Gravatar Pierre-Marie Pédrot2014-11-22
* Exporting a primitive allowing to run completely the tactic monad.Gravatar Pierre-Marie Pédrot2014-11-22
* Exporting the function handling side-effects only applied to terms.Gravatar Pierre-Marie Pédrot2014-11-20
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* new: Optimize Proof, Optimize HeapGravatar Enrico Tassi2014-11-09
* Follow up to experimental eager evar unification in bcba6d1bc9:Gravatar Hugo Herbelin2014-11-08
* Removing the legacy intro tactic code.Gravatar Pierre-Marie Pédrot2014-11-07
* Removing the old rename tactic.Gravatar Pierre-Marie Pédrot2014-11-04
* 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
* Cleaning and documenting Clenv.make_evar_clauseGravatar Pierre-Marie Pédrot2014-10-27
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* VarInstance are also goals.Gravatar Hugo Herbelin2014-10-25
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Monad: change the error managing of two-list combinators.Gravatar Arnaud Spiwack2014-10-23
* Evd.future_goals: forgot to revert the list in two places.Gravatar Arnaud Spiwack2014-10-23
* Proofview: forgot to change an exception after refactoring in ( 9f51aafebd5f3...Gravatar Arnaud Spiwack2014-10-23
* Specializing tclBREAK so that it can choose the return exception in caseGravatar Pierre-Marie Pédrot2014-10-22
* 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.mli: no more reference to Goal.goal.Gravatar Arnaud Spiwack2014-10-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 01:04:34 +0000