aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/miscprint.ml
Commit message (Expand)AuthorAge
* Attempt to improve error message when "apply in" fail.Gravatar Hugo Herbelin2017-03-15
* Fixing printing of pat%constr.Gravatar Hugo Herbelin2016-06-16
* Revert "Fixing printing of pat%constr."Gravatar Hugo Herbelin2016-04-27
* Revert "Protect printing of intro-patterns from collision when "[|" or "|]""Gravatar Hugo Herbelin2016-04-27
* Revert "Revert "Protect printing of intro-patterns from collision when "[|" or"Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing extra space in front of terminal in printing vernac."Gravatar Hugo Herbelin2016-04-27
* Fixing extra space in front of terminal in printing vernac.Gravatar Hugo Herbelin2016-04-27
* Revert "Protect printing of intro-patterns from collision when "[|" orGravatar Hugo Herbelin2016-04-27
* Protect printing of intro-patterns from collision when "[|" or "|]"Gravatar Hugo Herbelin2016-04-27
* Fixing printing of pat%constr.Gravatar Hugo Herbelin2016-04-27
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
* | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02