index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
Commit message (
Expand
)
Author
Age
*
Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ...
Maxime Dénès
2018-03-06
|
\
*
\
Merge PR #6896: [compat] Remove NOOP deprecated options.
Maxime Dénès
2018-03-06
|
\
\
*
\
\
Merge PR #6824: Remove deprecated options related to typeclasses.
Maxime Dénès
2018-03-06
|
\
\
\
*
\
\
\
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-05
|
\
\
\
\
|
|
|
*
|
[compat] Remove NOOP and alias deprecated options.
Emilio Jesus Gallego Arias
2018-03-04
|
|
*
|
|
Remove deprecated options related to typeclasses.
Théo Zimmermann
2018-03-04
|
|
|
/
/
*
|
|
|
Merge PR #935: Handling evars in the VM
Maxime Dénès
2018-03-04
|
\
\
\
\
|
|
_
|
/
/
|
/
|
|
|
*
|
|
|
Merge PR #6791: Removing compatibility support for versions older than 8.5.
Maxime Dénès
2018-03-04
|
\
\
\
\
*
\
\
\
\
Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ...
Maxime Dénès
2018-03-04
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #915: Fix rewrite in * side conditions
Maxime Dénès
2018-03-04
|
\
\
\
\
\
\
|
|
|
|
*
|
|
Removing test for bug #2850.
Pierre-Marie Pédrot
2018-03-03
|
|
|
|
*
|
|
Adding a test file for evar handling in the VM.
Pierre-Marie Pédrot
2018-03-03
|
|
|
*
|
|
|
Remove 8.5 compatibility support.
Théo Zimmermann
2018-03-02
|
|
|
*
|
|
|
Remove VOld compatibility flag.
Théo Zimmermann
2018-03-02
|
|
|
*
|
|
|
Turn warning for deprecated notations on.
Théo Zimmermann
2018-03-02
|
|
|
|
/
/
/
|
|
*
/
/
/
Fix #6878: univ undefined for [with Definition] bad instance size.
Gaëtan Gilbert
2018-03-01
|
|
|
/
/
/
|
*
/
/
/
Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".
Hugo Herbelin
2018-03-01
|
|
/
/
/
*
/
/
/
[test-suite] Add a basic test-case for `Load`.
Emilio Jesus Gallego Arias
2018-02-28
|
/
/
/
*
|
|
Merge PR #6756: Fix issue with spurious timing test failures
Maxime Dénès
2018-02-28
|
\
\
\
*
\
\
\
Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit...
Maxime Dénès
2018-02-28
|
\
\
\
\
|
|
|
*
|
Update headers following #6543.
Théo Zimmermann
2018-02-27
|
|
_
|
/
/
|
/
|
|
|
|
|
*
|
[test-suite] Move sed scripts into bash arrays
Jason Gross
2018-02-24
*
|
|
|
Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).
Maxime Dénès
2018-02-24
|
\
\
\
\
*
\
\
\
\
Merge PR #6599: Decimals in prelude
Maxime Dénès
2018-02-24
|
\
\
\
\
\
|
|
|
*
|
|
Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).
Hugo Herbelin
2018-02-23
|
|
_
|
/
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`
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 #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
|
\
\
\
\
\
\
\
\
|
|
|
|
|
*
|
|
|
Update SearchPattern.out for numeral notations
Jason Gross
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
|
|
|
*
|
|
|
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
|
|
|
*
|
|
|
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
|
|
|
*
|
|
|
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
|
|
|
*
|
|
|
In printing notations with "match", reasoning up to the order of clauses.
Hugo Herbelin
2018-02-20
|
|
|
*
|
|
|
Supporting recursive notations reversing the left-to-right order.
Hugo Herbelin
2018-02-20
|
|
|
*
|
|
|
Allowing variables used in recursive notation to occur several times in pattern.
Hugo Herbelin
2018-02-20
|
|
|
*
|
|
|
Allows recursive patterns for binders to be associative on the left.
Hugo Herbelin
2018-02-20
|
|
|
*
|
|
|
Fixing/improving notations with recursive patterns.
Hugo Herbelin
2018-02-20
|
|
|
*
|
|
|
Using name given by user to name a 'pat, if any.
Hugo Herbelin
2018-02-20
[next]
Maxime Dénès
Emilio Jesus Gallego Arias
Théo Zimmermann
Pierre-Marie Pédrot
Gaëtan Gilbert
Hugo Herbelin
Jason Gross