aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2015-01-13Made -print-mod-uid more silent and robust.Maxime Dénès
2015-01-12Add -no-native-compiler flag to list dumped by --help.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2015-01-11Avoiding a redundant information in unification error message.Hugo Herbelin
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2015-01-06rename: vi -> vioEnrico Tassi
2015-01-06Fix some documentation typos.Guillaume Melquiond
2015-01-05kernel/ind Change interface of declare_mind and declare_mutualMatthieu Sozeau
2015-01-05In Show Universes, print universes before normalization.Matthieu Sozeau
2014-12-29Fixing bug #3632 for good.Pierre-Marie Pédrot
2014-12-29Proof using: do not clear letins (unless they use a cleared var)Enrico Tassi
2014-12-28Proof using: call "clear" to remove from sight the vars not selectedEnrico Tassi
2014-12-28remove debug prints (leftover)Enrico Tassi
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 16:03:26 +0000