aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Update headers.Gravatar Maxime Dénès2015-01-12
* Avoiding a redundant information in unification error message.Gravatar Hugo Herbelin2015-01-11
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-01-06
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
* In Show Universes, print universes before normalization.Gravatar Matthieu Sozeau2015-01-05
* Fixing bug #3632 for good.Gravatar Pierre-Marie Pédrot2014-12-29
* Proof using: do not clear letins (unless they use a cleared var)Gravatar Enrico Tassi2014-12-29
* Proof using: call "clear" to remove from sight the vars not selectedGravatar Enrico Tassi2014-12-28
* remove debug prints (leftover)Gravatar Enrico Tassi2014-12-28
* Better doc and a few fixes for Proof using.Gravatar Enrico Tassi2014-12-19
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
* STM: rename and simplify flagsGravatar Enrico Tassi2014-12-17
* Arguments: warn only if no option is given (Close 3860)Gravatar Enrico Tassi2014-12-17
* Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Error messages of Searchxxx are coherent with goal selector.Gravatar Pierre Courtieu2014-12-16
* Failing on unbound notation variable in notation level modifiersGravatar Hugo Herbelin2014-12-15
* About now accepts hypothesis names and goal selector.Gravatar Pierre Courtieu2014-12-15
* Util.un_op -> Option.defaultGravatar Pierre Boutillier2014-12-14
* Searchxxx now interpret patterns in goal environment if any.Gravatar Pierre Courtieu2014-12-12
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
* Added a CannotSolveConstraint unification error and made experimentsGravatar Hugo Herbelin2014-12-11
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 09:19:46 +0000