diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-13 14:29:06 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-13 14:29:06 -0400 |
| commit | 673399a0aa43c94e5a3112164a6b373c61a2ae7a (patch) | |
| tree | a5c925f584f22ce41fb6cd243605e89ee0aa0a15 | |
| parent | 96b3d9d79c24bc3797327da56af82fc2f6b5e87b (diff) | |
Remove dead code in comments
| -rw-r--r-- | src/Compilers/Named/DeadCodeElimination.v | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/src/Compilers/Named/DeadCodeElimination.v b/src/Compilers/Named/DeadCodeElimination.v index c2e1e8a7d..19ccdf58f 100644 --- a/src/Compilers/Named/DeadCodeElimination.v +++ b/src/Compilers/Named/DeadCodeElimination.v @@ -27,32 +27,9 @@ Section language. Local Notation exprf := (@exprf base_type_code op (fun _ => Name)). Local Notation expr := (@expr base_type_code op (fun _ => Name)). Local Notation Expr := (@Expr base_type_code op). - (*Local Notation lexprf := (@Syntax.exprf base_type_code op (fun _ => list (option Name))). - Local Notation lexpr := (@Syntax.expr base_type_code op (fun _ => list (option Name))).*) Local Notation nexprf := (@Named.exprf base_type_code op Name). Local Notation nexpr := (@Named.expr base_type_code op Name). - (*Definition get_live_namesf (names : list (option Name)) {t} (e : lexprf t) : list (option Name) - := filter_live_namesf - base_type_code op - (option Name) None - (fun x y => match x, y with - | Some x, _ => Some x - | _, Some y => Some y - | None, None => None - end) - nil names e. - Definition get_live_names (names : list (option Name)) {t} (e : lexpr t) : list (option Name) - := filter_live_names - base_type_code op - (option Name) None - (fun x y => match x, y with - | Some x, _ => Some x - | _, Some y => Some y - | None, None => None - end) - nil names e.*) - Definition CompileAndEliminateDeadCode {t} (e : Expr t) (ls : list Name) : option (nexpr t) |