diff options
| author | herbelin | 2011-03-05 16:42:27 +0000 |
|---|---|---|
| committer | herbelin | 2011-03-05 16:42:27 +0000 |
| commit | 2118e320c272d88d01eab650e0dd0e83597230e1 (patch) | |
| tree | 403ef55a7fffe8ddba42f57ad9b2e47c7ce93d9c /pretyping/pretype_errors.ml | |
| parent | 4e5c9882c74b04e69ef885db7c05ed31bf6a2732 (diff) | |
Reorganized a bit evarconv.ml:
- Made a distinction between truly rigid constructions (Rigid) and
possibly flexible constructions (match/fix/meta, now called
PseudoRigid) that are currently assimilated to rigid by lack of
appropriate study of their flexibility. One day, the flexibility of
these pseudo-rigid constructions will have to considered seriously.
- Removed useless Cast/Cast cases in Rigid/Rigid block (Cast
are removed in advance and LetIn are not considered Rigid).
- Moved LetIn into the MaybeFlexible class.
- Moved the Lambda/Lambda case upwards to factorize the rules for
eta-expansion.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13882 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretype_errors.ml')
0 files changed, 0 insertions, 0 deletions
