index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
interp
Age
Commit message (
Expand
)
Author
2020-03-19
Merge PR #11795: Print implicit arguments in types of references
Hugo Herbelin
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-03-12
Print implicit arguments in types of references
SimonBoulier
2020-03-03
[exninfo] Deprecate aliases for exception re-raising.
Emilio Jesus Gallego Arias
2020-02-27
Merge PR #11650: Set Printing Parens
Emilio Jesus Gallego Arias
2020-02-25
Fixing residual bug of #11120.
Hugo Herbelin
2020-02-23
Not iterating recursive notations more than once.
Hugo Herbelin
2020-02-23
parens --> parentheses
Abhishek Anand (optiplex7010@home)
2020-02-23
added the new option
Abhishek Anand (optiplex7010@home)
2020-02-22
Fixes #4690: do not allow @f in notations when f is a notation variable.
Hugo Herbelin
2020-02-22
Inherit arguments scopes in pattern notations bound to some @id.
Hugo Herbelin
2020-02-22
In printing patterns, distinguish the case of a notation to @id.
Hugo Herbelin
2020-02-22
Inherit scopes and implicit sign. in notations for partially applied pattern.
Hugo Herbelin
2020-02-22
Fix index bug in computing implicit signature of abbrev. in pattern printing.
Hugo Herbelin
2020-02-22
Fix inheritance of argument scopes when printing notations in patterns.
Hugo Herbelin
2020-02-22
Use auxiliary function for externing record patterns.
Hugo Herbelin
2020-02-22
Inherit argument scopes in notations to expressions of the form @f.
Hugo Herbelin
2020-02-22
Propagate implicit arguments in all notations for partial applications.
Hugo Herbelin
2020-02-22
Deactivate implicit arguments in printing notations bound to "@f".
Hugo Herbelin
2020-02-22
Fixing printing of notations bound to an expression of the form "@f".
Hugo Herbelin
2020-02-22
Fixing a notation printing bug (missing a @ to reflect absence of imp. args).
Hugo Herbelin
2020-02-22
Fixing anomaly from #11091 (incompatible printing with notation and imp. args).
Hugo Herbelin
2020-02-22
Merge PR #11635: Cleanup around the tolerability structure
Emilio Jesus Gallego Arias
2020-02-22
Making structure of type "tolerability" and related clearer.
Hugo Herbelin
2020-02-21
Merge PR #11261: Use implicit types for printing (granting wish #10366).
Emilio Jesus Gallego Arias
2020-02-21
Merge PR #11142: Slightly improving strategy about when to print coercion or ...
Emilio Jesus Gallego Arias
2020-02-20
Merge PR #10832: Addressing #6082 and #7766: warning when overriding notation...
Emilio Jesus Gallego Arias
2020-02-19
Revert "Granting #9516 and #9518 (support for numerals and strings in custom ...
Hugo Herbelin
2020-02-19
Addressing #6082 and #7766 (overriding format of notation).
Hugo Herbelin
2020-02-19
Preparing fix to #6082 and #7766: Renaming type scope_elem and its elements.
Hugo Herbelin
2020-02-17
Take "Implicit Types" into account when printing terms.
Hugo Herbelin
2020-02-17
Mini-improvements in when to skip coercions or explicitly print implicit args.
Hugo Herbelin
2020-02-16
Granting #9516 and #9518 (support for numerals and strings in custom entries).
Hugo Herbelin
2020-02-13
Merge PR #11098: Let Arguments support anonymous implicit arguments
Emilio Jesus Gallego Arias
2020-02-13
Merge PR #11521: Remove Goptions.opt_name field
Pierre-Marie Pédrot
2020-02-13
Arguments: removing the restriction to set an anonymous parameter implicit.
Hugo Herbelin
2020-02-13
Implicit arguments: Fixing count of the position in compute_implicit_statuses.
Hugo Herbelin
2020-02-12
Remove Goptions.opt_name field
Gaëtan Gilbert
2020-02-12
Standardize constr -> globref operations to use destRef/isRef/isRefX
Gaëtan Gilbert
2020-02-11
Fixing some residual bugs of PR #10202 (manual implicit args in subterms).
Hugo Herbelin
2020-02-11
Reinforcing the role of type "typing_constraint".
Hugo Herbelin
2020-02-04
Correct bug in non max local implicit arguments
SimonBoulier
2020-02-04
Add syntax for non maximally inserted implicit arguments
SimonBoulier
2020-01-30
Constrextern.ml: Move a function earlier to be usable for pattern printing.
Hugo Herbelin
2020-01-30
Minor indentation change.
Hugo Herbelin
2020-01-30
Refactoring code for matching partial applications against notations.
Hugo Herbelin
2020-01-30
Refactoring code for externing applications.
Hugo Herbelin
2020-01-30
Constrextern.ml: for readability, use auxiliary function for externing records.
Hugo Herbelin
2020-01-08
Trailing implicit: Maxime's suggestions
SimonBoulier
2020-01-07
Turn trailing implicit warning into an error
SimonBoulier
[next]