index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
success
/
Injection.v
Age
Commit message (
Expand
)
Author
2018-10-02
Update the -compat flags
Jason Gross
2016-12-22
Fixing injection in the presence of let-in in constructors.
Hugo Herbelin
2016-10-03
fixing bug 4609: document an option governing the generation of equalities
Yves Bertot
2016-06-18
Giving a more natural semantics to injection by default.
Hugo Herbelin
2016-06-18
Exporting a generic argument induction_arg. As a consequence,
Hugo Herbelin
2016-02-13
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-25
Fixing an "injection as" bug in the presence of side conditions.
Hugo Herbelin
2015-04-01
Fixing test-suite.
Pierre-Marie Pédrot
2014-05-31
More on injection over a projectable "existT". - Fixing syntax "injection ......
Hugo Herbelin
2013-07-10
Continuing r16621 on injection intro-patterns:
herbelin
2013-07-09
Revising r16550 about providing intro patterns for applying injection:
herbelin
2013-06-02
Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as an
herbelin
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2008-06-21
- Implantation de la suggestion 1873 sur discriminate. Au final,
herbelin
2006-10-01
Une passe sur l'injection et la discrimination...
herbelin
2005-12-21
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
herbelin
2003-05-21
Nouveaux tests
herbelin
2001-10-15
*** empty log message ***
herbelin
