diff options
| author | herbelin | 2000-10-06 14:59:49 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-06 14:59:49 +0000 |
| commit | 96b11e6044168c84ddabf405394a0c16335e2b33 (patch) | |
| tree | f700b41100a5ca5afd90a04233e2a4fc5aa36fd3 /kernel | |
| parent | 69587312a973f868fec3cea58b20c9d4fb575df9 (diff) | |
Bug splay_prod_assum
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@668 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/reduction.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 71edc098a6..9d9f618458 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -986,8 +986,8 @@ let splay_prod_assum env sigma = | IsProd (x,t,c) -> prodec_rec (Sign.add_rel_decl (x,outcast_type t) l) c | IsLetIn (x,b,t,c) -> prodec_rec (Sign.add_rel_def (x,b,outcast_type t) l) c | IsCast (c,_) -> prodec_rec l c - | _ -> l,c - in + | _ -> l,t + in prodec_rec Sign.empty_rel_context let splay_arity env sigma c = |