index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Merge PR #6819: Document Arguments extra scopes flag
Maxime Dénès
2018-02-24
|
\
*
\
Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).
Maxime Dénès
2018-02-24
|
\
\
*
\
\
Merge PR #6803: coqdev.el: add space at the end of compile-command
Maxime Dénès
2018-02-24
|
\
\
\
*
\
\
\
Merge PR #6599: Decimals in prelude
Maxime Dénès
2018-02-24
|
\
\
\
\
*
\
\
\
\
Merge PR #6745: [ast] Improve precision of Ast location recognition in serial...
Maxime Dénès
2018-02-24
|
\
\
\
\
\
|
|
|
|
|
*
Document Arguments extra scopes flag
Jasper Hugunin
2018-02-22
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
*
|
|
|
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2018-02-22
|
/
/
/
/
*
|
|
|
Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`
Maxime Dénès
2018-02-21
|
\
\
\
\
*
\
\
\
\
Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_pred
Maxime Dénès
2018-02-21
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6767: [ci] add elpi
Maxime Dénès
2018-02-21
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)
Maxime Dénès
2018-02-21
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6283: A pre-commit hook to magically fix whitespace issues.
Maxime Dénès
2018-02-21
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just the...
Maxime Dénès
2018-02-21
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #6740: Adding a sanity check on inductive variance subtyping.
Maxime Dénès
2018-02-21
|
\
\
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
|
|
*
|
coqdev.el: add space at the end of compile-command
Gaëtan Gilbert
2018-02-21
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
Add CHANGES entry for decimals in prelude
Jason Gross
2018-02-20
|
|
|
|
|
|
|
|
*
|
Update SearchPattern.out for numeral notations
Jason Gross
2018-02-20
|
|
|
|
|
|
|
|
*
|
Doc: add Decimal-related files to index-list.html.template
Jason Gross
2018-02-20
|
|
|
|
|
|
|
|
*
|
Decimal goodies : conversion to/from Coq strings
Pierre Letouzey
2018-02-20
|
|
|
|
|
|
|
|
*
|
Decimal: proofs that conversions from/to nat,N,Z are bijections
Pierre Letouzey
2018-02-20
|
|
|
|
|
|
|
|
*
|
Decimal: simple representation of base-10 numbers
Pierre Letouzey
2018-02-20
|
|
_
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
Fixes bug #6774 (anomaly with ill-typed template polymorphism).
Hugo Herbelin
2018-02-20
|
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
Adding a test for wish #5532.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Documenting use of primitive entry names for restricting syntax in notations.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Extended documentation for notations referring to binders.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Trying a hack to support {'pat|P} without breaking compatibility.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Change default for notations with variables bound to both terms and binders.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Notations: Adding modifiers to tell which kind of binder a constr can parse.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Notations: A step in cleaning constr_entry_key.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
More flexibility in locating or referring to a notation.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
More structured printing in unicode notations for binders.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Being more flexible on format Adding a warning to be more informative
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
User-level support for Gonthier-Ssreflect's "if t then pat then u else v".
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
When printing a notation with "match", more flexibility in matching equations.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Adding general support for irrefutable disjunctive patterns.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Using an "as" clause when needed for printing irrefutable patterns.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Refining the strategy for glueing let-ins to a sequence of binders.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
A (significant) simplification in printing notations with recursive binders.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Respecting the ident/pattern distinction in notation modifiers.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
A first step at refreshing and documenting the new feature.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Adding support for parsing subterms of a notation as "pattern".
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Adding patterns in the category of binders for notations.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Preliminary work before adding general support for patterns in notations II.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Preliminary work before adding general support for patterns in notations I.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Preliminary work before extending support for binders in notations
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Preliminary steps before adding general support for patterns in notations.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
In printing notations with "match", reasoning up to the order of clauses.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Preliminary work before extending support for binders in notations
Hugo Herbelin
2018-02-20
[next]