index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
printing
/
ppconstr.ml
Commit message (
Expand
)
Author
Age
*
[toplevel] Remove duplicate beautify flags.
Emilio Jesus Gallego Arias
2016-10-17
*
Moving Pp.comments to CLexer so that Pp is purer (no more side-effect
Hugo Herbelin
2016-10-09
*
Fixing a beautifier bug pointed out by Emilio.
Hugo Herbelin
2016-10-05
*
Fix bug #4869, allow Prop, Set, and level names in constraints.
Matthieu Sozeau
2016-09-29
*
Fix tagging of notations.
Pierre-Marie Pédrot
2016-08-29
*
Complementing previous commit on fixes for printing binding patterns.
Hugo Herbelin
2016-07-19
*
Some extra fixes in printing patterns in binders.
Hugo Herbelin
2016-07-19
*
Taking into account binding patterns when agglutinating sequences of binders.
Hugo Herbelin
2016-07-19
*
Fixing missing parentheses in printing of patterns in binders.
Hugo Herbelin
2016-07-19
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Adding ability to put any pattern in binders, prefixed by a quote.
Daniel de Rauglaudre
2016-06-27
*
Fixing printing of Instance.
Hugo Herbelin
2016-06-16
*
Revert "A heuristic to add parentheses in the presence of rules such as"
Hugo Herbelin
2016-04-27
*
Revert "Temporary deactivate re-interpretation of terms in beautify."
Hugo Herbelin
2016-04-27
*
Revert "Fixing printing of Instance."
Hugo Herbelin
2016-04-27
*
Fixing printing of Instance.
Hugo Herbelin
2016-04-27
*
Temporary deactivate re-interpretation of terms in beautify.
Hugo Herbelin
2016-04-27
*
A heuristic to add parentheses in the presence of rules such as
Hugo Herbelin
2016-04-27
*
Supporting "(@foo) args" in patterns, where "@foo" has no arguments.
Hugo Herbelin
2016-03-13
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
CLEANUP: removing unused field
Matej Kosik
2016-01-11
*
|
Remove some unused functions.
Guillaume Melquiond
2016-01-02
*
|
Do not compose "str" and "to_string" whenever possible.
Guillaume Melquiond
2015-12-22
*
|
CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified
Matej Kosik
2015-12-18
|
/
*
Improving over printing of let-tuple (see #4447).
Hugo Herbelin
2015-12-03
*
Univs: add Strict Universe Declaration option (on by default)
Matthieu Sozeau
2015-10-07
*
Add a space in cast since cast binds loosely.
Gregory Malecha
2015-06-24
*
Update headers.
Maxime Dénès
2015-01-12
*
Fixing printing of dirpathes in Ppconstr. It was reversed.
Pierre-Marie Pédrot
2014-11-30
*
Adding tag output to references in Ppconstr.
Pierre-Marie Pédrot
2014-11-25
*
Adding notation terminals to coqtop highlight.
Pierre-Marie Pédrot
2014-11-17
*
Fixing semantics of Ppconstr.print_hunks.
Pierre-Marie Pédrot
2014-11-17
*
Missing keywords in Ppconstr.
Pierre-Marie Pédrot
2014-11-17
*
Moving printing code for red_expr and may_eval to Pptactic.
Pierre-Marie Pédrot
2014-11-17
*
Default styles for printing tags.
Pierre-Marie Pédrot
2014-11-17
*
Enforcing a stronger difference between the two syntaxes "simpl
Hugo Herbelin
2014-11-16
*
Additional style tags for constrs.
Pierre-Marie Pédrot
2014-11-15
*
Setting a keyword tag in Ppconstr.
Pierre-Marie Pédrot
2014-11-15
*
Plug the dynamic tags in the Richpp mechanism.
Pierre-Marie Pédrot
2014-11-10
*
lib/RichPp: Rename into Richpp.
Yann Régis-Gianas
2014-11-05
*
lib/Ppconstr: Cosmetics.
Regis-Gianas
2014-11-04
*
lib/Pp.tag: New.
Regis-Gianas
2014-11-04
*
printing/Ppannotation: Introduce a new annotation for keywords.
Regis-Gianas
2014-11-04
*
Ppannotation: New.
Regis-Gianas
2014-11-04
*
printing/Ppconstr.Make:
Regis-Gianas
2014-11-04
*
printing/Ppconstr.print_hunks:
Regis-Gianas
2014-11-04
*
printing/Ppconstr: Cosmetics.
Regis-Gianas
2014-11-04
*
Add syntax for naming new goals in refine: writing ?[id] instead of _
Hugo Herbelin
2014-09-30
*
Printing evar instance in a more intuitive order.
Hugo Herbelin
2014-09-29
[next]