aboutsummaryrefslogtreecommitdiff
path: root/proofs/proofview.ml
AgeCommit message (Expand)Author
2016-10-20A fix for #5097 (status of evars refined by "clear" in ltac: closed wrt evars).Hugo Herbelin
2016-10-12Merge remote-tracking branch 'git/bug5123' into v8.5Matthieu Sozeau
2016-10-11Fix bug #5123: mark all shelved evars unresolvableMatthieu Sozeau
2016-10-11Fix for bug #4863, update the Proofview's env withMatthieu Sozeau
2016-10-10Fix #4416: - Incorrect "Error: Incorrect number of goals"Arnaud Spiwack
2016-09-01Fixing name of internal refine ("simple refine").Hugo Herbelin
2016-05-16Fix bug #4737: cycle tactic doesn't like zero goals.Pierre-Marie Pédrot
2016-03-23Revert "refine: do check all unif problems are solved (Close: #4415, #4532)"Enrico Tassi
2016-03-23refine: do check all unif problems are solved (Close: #4415, #4532)Enrico Tassi
2016-02-17Fixing the Proofview.Goal.goal function.Pierre-Marie Pédrot
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-09The unshelve tactical now takes future goals into account.Pierre-Marie Pédrot
2015-12-09Adding an unshelve tactical.Pierre-Marie Pédrot
2015-11-12Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.Pierre-Marie Pédrot
2015-11-02Made that the syntax [id]:tac also applies to the shelve, which is after all ...Hugo Herbelin
2015-07-27Slightly improving line break formatting in Info command.Hugo Herbelin
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-02-24[Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...Arnaud Spiwack
2015-02-23Fix some typos in comments.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2015-01-08Fixed and extend bullet related info/error messages. + doc.Pierre Courtieu
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-12Make sure the goals on the shelve are identified as goal and unresolvable for...Arnaud Spiwack
2014-12-07Exporting store of goals so that new_evar in convert, intro, etc. canHugo Herbelin
2014-12-04Occur-check in refine.Arnaud Spiwack
2014-12-04Refine primitive: [unsafe] is now true by default.Arnaud Spiwack
2014-12-04Some refactoring following previous commit.Arnaud Spiwack
2014-12-04Better implementation of 4a858a51322f2dd488b02130ca82ebcc4dc9ca35.Arnaud Spiwack
2014-12-04Factoring 2ee213b824dda48c3fe60e95316daf09f07e8075.Arnaud Spiwack
2014-11-30Fixing bug #3682.Pierre-Marie Pédrot
2014-11-30Adding missing unsafe primitives to Proofview.Pierre-Marie Pédrot
2014-11-28Tactic primitives: missing [advance] lead to spurious dangling goals.Arnaud Spiwack
2014-11-22Exporting a primitive allowing to run completely the tactic monad.Pierre-Marie Pédrot
2014-11-09new: Optimize Proof, Optimize HeapEnrico Tassi
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-25VarInstance are also goals.Hugo Herbelin
2014-10-23Monad: change the error managing of two-list combinators.Arnaud Spiwack
2014-10-23Proofview: forgot to change an exception after refactoring in ( 9f51aafebd5f3...Arnaud Spiwack
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 14:42:21 +0000