index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
success
/
primitiveproj.v
Commit message (
Expand
)
Author
Age
*
Add test-suite case for performance, had to use Timeout
Matthieu Sozeau
2018-06-15
*
[compat] Remove NOOP and alias deprecated options.
Emilio Jesus Gallego Arias
2018-03-04
*
test-suite: more use of the new command Extraction TestCompile
Pierre Letouzey
2017-07-27
*
Prelude : no more autoload of plugins extraction and recdef
Pierre Letouzey
2017-06-14
*
Fixed bug #4622.
Matthieu Sozeau
2016-07-06
*
Disallow dependent case on prim records w/o eta
Matthieu Sozeau
2016-07-06
*
Primitive projections: protect kernel from erroneous definitions.
Matthieu Sozeau
2016-03-10
*
Fixing logical bugs in the presence of let-ins in computiong primitive
Hugo Herbelin
2015-11-18
*
Extraction: fix primitive projection extraction.
Matthieu Sozeau
2015-07-22
*
Revert specific syntax for primitive projections, avoiding ugly
Matthieu Sozeau
2014-09-17
*
Parsing and printing of primitive projections, fix buggy behavior when
Matthieu Sozeau
2014-09-10
*
- Fix printing and parsing of primitive projections, including the Set
Matthieu Sozeau
2014-09-09
*
Fix primitive projections declarations for inductive records.
Matthieu Sozeau
2014-09-05
*
Simplify even further the declaration of primitive projections,
Matthieu Sozeau
2014-08-30