diff options
| author |  Jason Gross <jagro@google.com> | 2018-08-02 17:47:51 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-08-02 17:47:51 -0400 |
| commit | 25ddf0a94f472ae69641c99754a34c82b780bbf2 (patch) | |
| tree | 71ac7ae612e07307ead5fb88815baaf53485ba14 /src | |
| parent | 3a81efa9fd868310b209533fdb77b0d1b295f3a9 (diff) | |
Also generate decidable equality for pattern.ident
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v index 5c6b4faec..6b666c435 100644 --- a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v +++ b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v @@ -9,6 +9,7 @@ Module Compilers. Module pattern. Module ident. Set Boolean Equality Schemes. + Set Decidable Equality Schemes. (* Set Printing Coercions. Redirect "/tmp/pr" Print Compilers.ident.ident. @@ -706,6 +707,7 @@ Module Compilers. Module pattern. Module ident. Set Boolean Equality Schemes. + Set Decidable Equality Schemes. (""" + """* Set Printing Coercions. Redirect "/tmp/pr" Print Compilers.ident.ident. |