index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
printing
/
miscprint.ml
Commit message (
Expand
)
Author
Age
*
Attempt to improve error message when "apply in" fail.
Hugo Herbelin
2017-03-15
*
Fixing printing of pat%constr.
Hugo Herbelin
2016-06-16
*
Revert "Fixing printing of pat%constr."
Hugo Herbelin
2016-04-27
*
Revert "Protect printing of intro-patterns from collision when "[|" or "|]""
Hugo Herbelin
2016-04-27
*
Revert "Revert "Protect printing of intro-patterns from collision when "[|" or"
Hugo Herbelin
2016-04-27
*
Revert "Fixing extra space in front of terminal in printing vernac."
Hugo Herbelin
2016-04-27
*
Fixing extra space in front of terminal in printing vernac.
Hugo Herbelin
2016-04-27
*
Revert "Protect printing of intro-patterns from collision when "[|" or
Hugo Herbelin
2016-04-27
*
Protect printing of intro-patterns from collision when "[|" or "|]"
Hugo Herbelin
2016-04-27
*
Fixing printing of pat%constr.
Hugo Herbelin
2016-04-27
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
*
|
Stronger invariants on the use of the introduction pattern (pat1,...,patn).
Hugo Herbelin
2016-01-21
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
|
/
*
Update headers.
Maxime Dénès
2015-01-12
*
Seeing IntroWildcard as an action intro pattern rather than as a naming pattern
Hugo Herbelin
2014-09-30
*
Adding a new intro-pattern for "apply in" on the fly. Using syntax
Hugo Herbelin
2014-08-18
*
Reorganisation of intropattern code
Hugo Herbelin
2014-08-18
*
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
Pierre Letouzey
2014-03-02