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