aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v8
-rw-r--r--src/Experiments/NewPipeline/Rewriter.v6
2 files changed, 7 insertions, 7 deletions
diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
index c991c3454..ab610531f 100644
--- a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
+++ b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
@@ -89,8 +89,8 @@ Module Compilers.
(*
Set Printing Coercions.
- Redirect "/tmp/pr" Print Compilers.ident.ident.
- Redirect "/tmp/sm" Show Match Compilers.ident.ident.
+ (* Redirect "/tmp/pr" Print Compilers.ident.ident. *)
+ (* Redirect "/tmp/sm" Show Match Compilers.ident.ident. *)
*)
(*
<<<
@@ -905,8 +905,8 @@ Module Compilers.
(""" + """*
Set Printing Coercions.
- Redirect "/tmp/pr" Print Compilers.ident.ident.
- Redirect "/tmp/sm" Show Match Compilers.ident.ident.
+ (* Redirect "/tmp/pr" Print Compilers.ident.ident. *)
+ (* Redirect "/tmp/sm" Show Match Compilers.ident.ident. *)
*""" + """)
"""
diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v
index 1b66d6206..26a833aac 100644
--- a/src/Experiments/NewPipeline/Rewriter.v
+++ b/src/Experiments/NewPipeline/Rewriter.v
@@ -2190,7 +2190,7 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y)
Local Set Printing Depth 1000000.
Local Set Printing Width 200.
Import RewriterPrintingNotations.
- Redirect "/tmp/fancy_rewrite_head" Print fancy_rewrite_head.
+ (* Redirect "/tmp/fancy_rewrite_head" Print fancy_rewrite_head. *)
End red_fancy.
Section red_nbe.
@@ -2286,7 +2286,7 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y)
Local Set Printing Depth 1000000.
Local Set Printing Width 200.
Import RewriterPrintingNotations.
- Redirect "/tmp/nbe_rewrite_head" Print nbe_rewrite_head.
+ (* Redirect "/tmp/nbe_rewrite_head" Print nbe_rewrite_head. *)
End red_nbe.
Section red_arith.
@@ -2383,7 +2383,7 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y)
Local Set Printing Depth 1000000.
Local Set Printing Width 200.
Import RewriterPrintingNotations.
- Redirect "/tmp/arith_rewrite_head" Print arith_rewrite_head.
+ (* Redirect "/tmp/arith_rewrite_head" Print arith_rewrite_head. *)
End red_arith.
Definition RewriteNBE {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t