index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
printing
Commit message (
Expand
)
Author
Age
*
Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...
Arnaud Spiwack
2015-09-25
*
Make inductives that were assumed positive appear in `Print Assumptions`.
Arnaud Spiwack
2015-06-24
*
Add corresponding field in `VernacInductive`.
Arnaud Spiwack
2015-06-24
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-06-24
|
\
|
*
Add a space in cast since cast binds loosely.
Gregory Malecha
2015-06-24
*
|
Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.
Thomas Sibut-Pinote
2015-06-23
*
|
Merge remote-tracking branch 'forge/v8.5'
Pierre Boutillier
2015-06-22
|
\
|
|
*
Make end-of-proof output consistent across toplevels.
Guillaume Melquiond
2015-06-19
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-05-05
|
\
|
|
*
Add a [Redirect] vernacular command
Clément Pit--Claudel
2015-05-04
|
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
*
|
Merge branch 'v8.5' into trunk
Pierre Letouzey
2015-04-09
|
\
|
|
*
Declarative mode: plug the specialised printers back.
Arnaud Spiwack
2015-03-31
|
*
Better formatting of messages in proofs.
Arnaud Spiwack
2015-03-31
|
*
Generalisation of the "end command" argument of the goal printer.
Arnaud Spiwack
2015-03-31
*
|
Merge branch 'v8.5' into trunk
Enrico Tassi
2015-03-30
|
\
|
|
*
Putting the From parameter of the Require command into the AST.
Pierre-Marie Pédrot
2015-03-27
|
*
rewiring Czar printers that were disabled
Pierre Corbineau
2015-03-13
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-03-11
|
\
|
|
*
Do not display the status of monomorphic constants unless in universe-polymor...
Guillaume Melquiond
2015-03-09
*
|
rewiring Czar printers that were disabled
Pierre Corbineau
2015-03-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-02-23
|
\
|
|
*
Better English for #4070 implicit arguments message (thanks to Jason for his ...
Hugo Herbelin
2015-02-21
|
*
An answer to #4070 (message for implicit arguments of inl not clear).
Hugo Herbelin
2015-02-20
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-02-15
|
\
|
|
*
Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior
Enrico Tassi
2015-02-14
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-02-10
|
\
|
|
*
More efficient Richpp.
Pierre-Marie Pédrot
2015-02-06
|
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
|
Merge branch 'v8.5' into trunk.
Pierre-Marie Pédrot
2015-01-25
|
\
|
|
*
Isolate a function for printing evar sets.
Hugo Herbelin
2015-01-24
*
|
Splitting ML tactics in one function per grammar entry.
Pierre-Marie Pédrot
2015-01-23
*
|
Embedding the index of the ML tactic entry in the Tacexpr AST.
Pierre-Marie Pédrot
2015-01-21
*
|
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-18
|
*
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-17
|
/
*
Fix issue in printing due to de Bruijn bug when constructing compatibility
Matthieu Sozeau
2015-01-13
*
Update headers.
Maxime Dénès
2015-01-12
*
Declarations.mli refactoring: module_type_body = module_body
Pierre Letouzey
2015-01-11
*
Continuing 785f82ee1 on reverting not only f5d7b2b1e but also
Hugo Herbelin
2015-01-08
*
Fixed and extend bullet related info/error messages. + doc.
Pierre Courtieu
2015-01-08
*
Revert "Term: include a function to print terms"
Enrico Tassi
2014-12-27
*
Term: include a function to print terms
Enrico Tassi
2014-12-26
*
A global [gfail] tactic which works like [fail] except that it fails even if ...
Arnaud Spiwack
2014-12-23
*
Fix compilation error in some configurations.
Arnaud Spiwack
2014-12-23
*
Add a backtracking version of Ltac's [match].
Arnaud Spiwack
2014-12-19
*
Proof using: New vernacular to name sets of section variables
Enrico Tassi
2014-12-18
*
Fixed bad newlines in output for std output and emacs.
Pierre Courtieu
2014-12-18
*
msg_info now puts infomsg tag in emacs mode.
Pierre Courtieu
2014-12-16
*
Changed bullet informations to warning for better display in PG.
Pierre Courtieu
2014-12-15
*
About now accepts hypothesis names and goal selector.
Pierre Courtieu
2014-12-15
[next]