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