aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofview.ml
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\
| * The unshelve tactical now takes future goals into account.Gravatar Pierre-Marie Pédrot2015-12-09
| * Adding an unshelve tactical.Gravatar Pierre-Marie Pédrot2015-12-09
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-15
|\|
| * Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.Gravatar Pierre-Marie Pédrot2015-11-12
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\|
| * Made that the syntax [id]:tac also applies to the shelve, which is after all ...Gravatar Hugo Herbelin2015-11-02
* | Removing the evar_map argument from s_enter.Gravatar Pierre-Marie Pédrot2015-10-29
* | Proofview.Goal.sigma returns an indexed evarmap.Gravatar Pierre-Marie Pédrot2015-10-20
* | Indexing Proofview.goals with a stage.Gravatar Pierre-Marie Pédrot2015-10-20
* | Boxing the Goal.enter primitive into a record type.Gravatar Pierre-Marie Pédrot2015-10-20
* | Renaming Goal.enter field into s_enter.Gravatar Pierre-Marie Pédrot2015-10-20
* | Adding a monotonic variant of Goal.enter and Goal.nf_enter.Gravatar Pierre-Marie Pédrot2015-10-19
* | Making Evarutil.new_evar monotonous.Gravatar Pierre-Marie Pédrot2015-10-18
* | Constraining refine to monotonic functions.Gravatar Pierre-Marie Pédrot2015-10-18
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-29
|\|
| * Slightly improving line break formatting in Info command.Gravatar Hugo Herbelin2015-07-27
* | Exposing the minimal amount of internal of the Logic monad in order toGravatar Pierre-Marie Pédrot2015-05-06
|/
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* [Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...Gravatar Arnaud Spiwack2015-02-24
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixed and extend bullet related info/error messages. + doc.Gravatar Pierre Courtieu2015-01-08
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Make sure the goals on the shelve are identified as goal and unresolvable for...Gravatar Arnaud Spiwack2014-12-12
* 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
* Tactic primitives: missing [advance] lead to spurious dangling goals.Gravatar Arnaud Spiwack2014-11-28
* Exporting a primitive allowing to run completely the tactic monad.Gravatar Pierre-Marie Pédrot2014-11-22
* new: Optimize Proof, Optimize HeapGravatar Enrico Tassi2014-11-09
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 23:50:09 +0000