aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Improved tracking of the origin of evars.Gravatar Hugo Herbelin2014-12-07
* Improving error message when one instance-hole is not found.Gravatar Hugo Herbelin2014-12-04
* Reactivating option "Set Printing Existential Instances" for asking printing ...Gravatar Hugo Herbelin2014-12-04
* Slight improving of a unification error message.Gravatar Hugo Herbelin2014-12-03
* Adding a Refine Instance Mode option that allows to deactivate theGravatar Pierre-Marie Pédrot2014-11-30
* async_queries_* merged with async_proofs_*Gravatar Enrico Tassi2014-11-27
* Feedback: API cleaned up, documented and made user extensibleGravatar Enrico Tassi2014-11-27
* Plugging console highlighting in for toplevel and compilation error messages.Gravatar Pierre-Marie Pédrot2014-11-24
* Pass around information on the use of template polymorphism forGravatar Matthieu Sozeau2014-11-23
* Removing superfluous newlines in setoid_rewrite error message.Gravatar Hugo Herbelin2014-11-22
* Exporting the function handling side-effects only applied to terms.Gravatar Pierre-Marie Pédrot2014-11-20
* Fixing a little bug with nested but convertible occurrences in "destruct at".Gravatar Hugo Herbelin2014-11-18
* Setting error tag on generic errors returned by Coqtop.Gravatar Pierre-Marie Pédrot2014-11-17
* For consistency with other coqtop flags, use -help rather than --help in usage.Gravatar Hugo Herbelin2014-11-16
* Removing a pperrnl.Gravatar Pierre-Marie Pédrot2014-11-15
* Adding a command line option to print out accepted color tags.Gravatar Pierre-Marie Pédrot2014-11-15
* Reworking the -color flag of coqtop.Gravatar Pierre-Marie Pédrot2014-11-15
* Plugging the color initialization in the Coqtop loop.Gravatar Pierre-Marie Pédrot2014-11-15
* Exit with code 129 when an anomaly occurs.Gravatar Xavier Clerc2014-11-14
* Fixing Scheme Equality, after bug introduced in bf018569405c.Gravatar Hugo Herbelin2014-11-13
* Continuing 3741c46fe134 on reporting ltac error.Gravatar Hugo Herbelin2014-11-08
* Now that evars can be parsed, protect strongly Check from calling kernel with...Gravatar Hugo Herbelin2014-11-03
* Show: do print the goalsGravatar Enrico Tassi2014-11-03
* Add an [Info Level] option to print info traces automatically.Gravatar Arnaud Spiwack2014-11-01
* Add [Info] command.Gravatar Arnaud Spiwack2014-11-01
* STM: new worker for queriesGravatar Enrico Tassi2014-10-31
* Show_script called only if in coqtop modeGravatar Enrico Tassi2014-10-31
* Fixes for PG (Close 3763, 3770)Gravatar Enrico Tassi2014-10-27
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Evd.future_goals: forgot to revert the list in two places.Gravatar Arnaud Spiwack2014-10-23
* Make rint_location_in_file resilient to Cd (close 3630)Gravatar Enrico Tassi2014-10-22
* Goal printing made uniform: always done in STM (close 3585)Gravatar Enrico Tassi2014-10-22
* Split [Proofview] into a file where the basic operations on the state are def...Gravatar Arnaud Spiwack2014-10-22
* Proofview: move more functions to the Unsafe module.Gravatar Arnaud Spiwack2014-10-22
* Remove the deprecated open-constr based refine.Gravatar Arnaud Spiwack2014-10-22
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-10-22
* Continuing experimental printing of the signature of open evars inGravatar Hugo Herbelin2014-10-21
* Now printing "now a keyword" only in verbose mode.Gravatar Hugo Herbelin2014-10-17
* Experimental printing of the signature of open evars in Check.Gravatar Hugo Herbelin2014-10-17
* Fix ML paths (thanks Jean-Marc Notin for bisecting it)Gravatar Enrico Tassi2014-10-14
* Fix typo, thanks Mike Shulman for spotting itGravatar Enrico Tassi2014-10-13
* Emit a warning for void Arguments statement (Close 3713)Gravatar Enrico Tassi2014-10-13
* STM: primitives to snapshot a .vi while in interactive modeGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Coqinit: look in toploop/ even if configured with -localGravatar Enrico Tassi2014-10-13
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Give the same argument name for the record binder of type classGravatar Matthieu Sozeau2014-10-10
* Add debug printers for projections, fix printing of evar constraintsGravatar Matthieu Sozeau2014-10-10
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 18:40:35 +0000