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
*
Getting rid of some hardwired generic arguments.
Pierre-Marie Pédrot
2015-12-17
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-08
|
\
*
|
Moving extended_rel_vect/extended_rel_list to the kernel.
Hugo Herbelin
2015-12-05
*
|
Getting rid of the dynamic node of the tactic AST.
Pierre-Marie Pédrot
2015-12-04
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-03
|
\
\
|
|
*
Improving over printing of let-tuple (see #4447).
Hugo Herbelin
2015-12-03
|
|
/
|
*
Dead code from August 2014 in apply in.
Hugo Herbelin
2015-12-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
|
\
|
|
*
Adding syntax "Show id" to show goal named id (shelved or not).
Hugo Herbelin
2015-11-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
|
*
Univs: local names handling.
Matthieu Sozeau
2015-10-28
|
*
Printing of @{} instances for polymorphic references in Print and About.
Matthieu Sozeau
2015-10-28
*
|
Type delayed_open_constr is now monotonic.
Pierre-Marie Pédrot
2015-10-19
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
|
\
|
|
*
Axioms now support the universe binding syntax.
Pierre-Marie Pédrot
2015-10-08
|
*
Goptions: new value type: optional string
Enrico Tassi
2015-10-08
|
*
Univs: add Strict Universe Declaration option (on by default)
Matthieu Sozeau
2015-10-07
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-06
|
\
|
|
*
Univs: fix printing bug #3797.
Matthieu Sozeau
2015-10-05
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-09-25
|
\
|
|
*
Print Assumptions shows engagement.
Maxime Dénès
2015-09-20
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-09-17
|
\
|
|
*
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-09-14
|
*
Revert the four previous commits and update the description of Richpp.
Pierre-Marie Pédrot
2015-08-15
|
*
More invariants in Richpp.
Pierre-Marie Pédrot
2015-08-15
|
*
More parametric type for generalized XML.
Pierre-Marie Pédrot
2015-08-15
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-07-27
|
\
|
|
*
Fixing bug #2169:
Pierre-Marie Pédrot
2015-07-27
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-07-18
|
\
|
|
*
Fixing printing of primitive coinductive record status.
Pierre-Marie Pédrot
2015-07-09
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-07-02
|
\
|
|
*
Assumptions: more informative print for False axiom (Close: #4054)
Enrico Tassi
2015-06-29
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-06-28
|
\
|
|
*
Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"
Lionel Rieg
2015-06-26
*
|
Remove other types not carried by interpretations in `Tacexpr`.
Arnaud Spiwack
2015-06-25
*
|
Remove useless `and_short_name` in interpreted level in `Tacexpr`.
Arnaud Spiwack
2015-06-25
|
*
Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.
Thomas Sibut-Pinote
2015-06-25
*
|
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
|
\
|
[next]