diff options
| author | filliatr | 1999-12-10 08:57:01 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-10 08:57:01 +0000 |
| commit | 85bd945e22abc31fec8f89da1779d94027323e91 (patch) | |
| tree | 356cfc0aa9a5f6b2328b05a4509d76bbd89a73e7 /kernel/reduction.ml | |
| parent | baa3e16836c3f0daf24ba47aadbdee525762d6ec (diff) | |
debug discharge et inductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@227 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 36 |
1 files changed, 0 insertions, 36 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index cbc3fe343e..195b4ce18f 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1309,39 +1309,3 @@ let rec whd_ise1_metas sigma = function | DOP2(Cast,c,_) -> whd_ise1_metas sigma c | c -> c - -(* Fonction spéciale qui laisse les cast clés sous les Fix ou les MutCase *) - -let under_outer_cast f = function - | DOP2 (Cast,b,t) -> DOP2 (Cast,f b,f t) - | c -> f c - -let rec strip_all_casts t = - match t with - | DOP2 (Cast, b, _) -> strip_all_casts b - | DOP0 _ as t -> t - (* Cas ad hoc *) - | DOPN(Fix _ as f,v) -> - let n = Array.length v in - let ts = Array.sub v 0 (n-1) in - let b = v.(n-1) in - DOPN(f, Array.append - (Array.map strip_all_casts ts) - [|under_outer_cast strip_all_casts b|]) - | DOPN(CoFix _ as f,v) -> - let n = Array.length v in - let ts = Array.sub v 0 (n-1) in - let b = v.(n-1) in - DOPN(f, Array.append - (Array.map strip_all_casts ts) - [|under_outer_cast strip_all_casts b|]) - | DOP1(oper,c) -> DOP1(oper,strip_all_casts c) - | DOP2(oper,c1,c2) -> DOP2(oper,strip_all_casts c1,strip_all_casts c2) - | DOPN(oper,cl) -> DOPN(oper,Array.map strip_all_casts cl) - | DOPL(oper,cl) -> DOPL(oper,List.map strip_all_casts cl) - | DLAM(na,c) -> DLAM(na,strip_all_casts c) - | DLAMV(na,c) -> DLAMV(na,Array.map (under_outer_cast strip_all_casts) c) - | VAR _ as t -> t - | Rel _ as t -> t - - |