aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretype_errors.ml
diff options
context:
space:
mode:
authorherbelin2011-03-05 16:42:27 +0000
committerherbelin2011-03-05 16:42:27 +0000
commit2118e320c272d88d01eab650e0dd0e83597230e1 (patch)
tree403ef55a7fffe8ddba42f57ad9b2e47c7ce93d9c /pretyping/pretype_errors.ml
parent4e5c9882c74b04e69ef885db7c05ed31bf6a2732 (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