diff options
| -rw-r--r-- | src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v index ab610531f..c991c3454 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. *""" + """) """ |