index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
Commit message (
Expand
)
Author
Age
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
Prevent spurious warnings about Arguments.
Guillaume Melquiond
2015-01-29
*
Equality Schemes options: reverting commit ff9f94634 which is
Hugo Herbelin
2015-01-24
*
Isolate a function for printing evar sets.
Hugo Herbelin
2015-01-24
*
Add the possibility of defining opaque terms with program.
mlasson
2015-01-21
*
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-17
*
Make native compiler handle universe polymorphic definitions.
Maxime Dénès
2015-01-17
*
Make -print-mod-uid accept a list of files.
Maxime Dénès
2015-01-15
*
Made -print-mod-uid more silent and robust.
Maxime Dénès
2015-01-13
*
Add -no-native-compiler flag to list dumped by --help.
Maxime Dénès
2015-01-12
*
Update headers.
Maxime Dénès
2015-01-12
*
Avoiding a redundant information in unification error message.
Hugo Herbelin
2015-01-11
*
Avoiding introducing yet another convention in naming files.
Hugo Herbelin
2015-01-08
*
rename: vi -> vio
Enrico Tassi
2015-01-06
*
Fix some documentation typos.
Guillaume Melquiond
2015-01-06
*
kernel/ind Change interface of declare_mind and declare_mutual
Matthieu Sozeau
2015-01-05
*
In Show Universes, print universes before normalization.
Matthieu Sozeau
2015-01-05
*
Fixing bug #3632 for good.
Pierre-Marie Pédrot
2014-12-29
*
Proof using: do not clear letins (unless they use a cleared var)
Enrico Tassi
2014-12-29
*
Proof using: call "clear" to remove from sight the vars not selected
Enrico Tassi
2014-12-28
*
remove debug prints (leftover)
Enrico Tassi
2014-12-28
*
Better doc and a few fixes for Proof using.
Enrico Tassi
2014-12-19
*
Proof using: New vernacular to name sets of section variables
Enrico Tassi
2014-12-18
*
STM: rename and simplify flags
Enrico Tassi
2014-12-17
*
Arguments: warn only if no option is given (Close 3860)
Enrico Tassi
2014-12-17
*
Fixing CAMLP4 compilation.
Pierre-Marie Pédrot
2014-12-16
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
Error messages of Searchxxx are coherent with goal selector.
Pierre Courtieu
2014-12-16
*
Failing on unbound notation variable in notation level modifiers
Hugo Herbelin
2014-12-15
*
About now accepts hypothesis names and goal selector.
Pierre Courtieu
2014-12-15
*
Util.un_op -> Option.default
Pierre Boutillier
2014-12-14
*
Searchxxx now interpret patterns in goal environment if any.
Pierre Courtieu
2014-12-12
*
Searchxxx now search also the hypothesis and support goal selector.
Pierre Courtieu
2014-12-12
*
Added a CannotSolveConstraint unification error and made experiments
Hugo Herbelin
2014-12-11
*
Tentatively more informative report of failure when inferring
Hugo Herbelin
2014-12-11
*
Switch the few remaining iso-latin-1 files to utf8
Pierre Letouzey
2014-12-09
*
Improved tracking of the origin of evars.
Hugo Herbelin
2014-12-07
*
Improving error message when one instance-hole is not found.
Hugo Herbelin
2014-12-04
*
Reactivating option "Set Printing Existential Instances" for asking printing ...
Hugo Herbelin
2014-12-04
*
Slight improving of a unification error message.
Hugo Herbelin
2014-12-03
*
Adding a Refine Instance Mode option that allows to deactivate the
Pierre-Marie Pédrot
2014-11-30
*
async_queries_* merged with async_proofs_*
Enrico Tassi
2014-11-27
*
Feedback: API cleaned up, documented and made user extensible
Enrico Tassi
2014-11-27
*
Plugging console highlighting in for toplevel and compilation error messages.
Pierre-Marie Pédrot
2014-11-24
*
Pass around information on the use of template polymorphism for
Matthieu Sozeau
2014-11-23
*
Removing superfluous newlines in setoid_rewrite error message.
Hugo Herbelin
2014-11-22
*
Exporting the function handling side-effects only applied to terms.
Pierre-Marie Pédrot
2014-11-20
*
Fixing a little bug with nested but convertible occurrences in "destruct at".
Hugo Herbelin
2014-11-18
*
Setting error tag on generic errors returned by Coqtop.
Pierre-Marie Pédrot
2014-11-17
*
For consistency with other coqtop flags, use -help rather than --help in usage.
Hugo Herbelin
2014-11-16
[next]