aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2014-12-19Better doc and a few fixes for Proof using.Enrico Tassi
2014-12-18Proof using: New vernacular to name sets of section variablesEnrico Tassi
2014-12-17STM: rename and simplify flagsEnrico Tassi
2014-12-17Arguments: warn only if no option is given (Close 3860)Enrico Tassi
2014-12-16Fixing CAMLP4 compilation.Pierre-Marie Pédrot
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-16Error messages of Searchxxx are coherent with goal selector.Pierre Courtieu
2014-12-15Failing on unbound notation variable in notation level modifiersHugo Herbelin
2014-12-15About now accepts hypothesis names and goal selector.Pierre Courtieu
2014-12-14Util.un_op -> Option.defaultPierre Boutillier
2014-12-12Searchxxx now interpret patterns in goal environment if any.Pierre Courtieu
2014-12-12Searchxxx now search also the hypothesis and support goal selector.Pierre Courtieu
2014-12-11Added a CannotSolveConstraint unification error and made experimentsHugo Herbelin
2014-12-11Tentatively more informative report of failure when inferringHugo Herbelin
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-12-07Improved tracking of the origin of evars.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 20:21:03 +0000