aboutsummaryrefslogtreecommitdiff
path: root/kernel/cemitcodes.mli
diff options
context:
space:
mode:
authorherbelin2011-12-04 20:48:32 +0000
committerherbelin2011-12-04 20:48:32 +0000
commit095eee7e2ae4a1715683e766af973c28500583f0 (patch)
tree1e053216380517db302e1ace1b7265887ccc5a7e /kernel/cemitcodes.mli
parente47cdbd232517adf6e6bf411b9f9715c43773fd5 (diff)
Fixed a small regression in pattern-matching compilation introduced in
r14737 (when to expand an alias). However, the heuristic remains different as before r14737 since we stopped taking into account the dependency in the predicate to take the decision of expanding or not. Let's see if we can eventually fine-tuning this. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14760 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/cemitcodes.mli')
0 files changed, 0 insertions, 0 deletions