diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-15 14:21:35 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-15 14:21:35 +0000 |
| commit | f172147decf35906708e4c0896f644ebca9c0eeb (patch) | |
| tree | 7057c726679fc2239b25c935d1f5b53495eaecbd /kernel | |
| parent | 09321f03913194960d3bb637f430052681849f3f (diff) | |
pattern-matching avec cas inutilise dans closure
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3148 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/closure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 2d30b2aa3..078f46b8d 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -884,7 +884,7 @@ let rec knh m stk = | (None, stk') -> (m,stk')) | FCast(t,_) -> knh t stk (* cases where knh stops *) - | (FFlex _|FLetIn _|FInd _|FConstruct _|FEvar _) -> (m, stk) + | (FFlex _|FLetIn _|FConstruct _|FEvar _) -> (m, stk) | (FRel _|FAtom _|FInd _) -> (set_norm m; (m, stk)) | (FLambda _|FCoFix _|FProd _) -> (set_whnf m; (m, stk)) |