diff options
| author | msozeau | 2008-03-18 22:44:14 +0000 |
|---|---|---|
| committer | msozeau | 2008-03-18 22:44:14 +0000 |
| commit | 489893c1ffc709023ada9c169106f2779919864a (patch) | |
| tree | f6c93b88dfbf091ec977a9ce2e71b4fe02ac9e96 /pretyping/typeclasses_errors.ml | |
| parent | 0d06d04e63919eb021721d42581169902d29612a (diff) | |
Implementation of rewriting under lambdas. Tested on exists only.
Adds some instances that incur again a small performance penalty because they cannot
be discriminated against for now (the discrimination net is considering
the head constructor to be Morphism).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10694 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions