diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-26 14:08:38 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-26 14:08:38 +0100 |
| commit | 4dabb8cd9b292bb873155e02e430f79cb43dc629 (patch) | |
| tree | b873bfe452f0819fe13ea333eca6c0dd8684aa8c /cparser | |
| parent | 9ce733bd06a6f36a144769b05b9405ea7ebbbfb9 (diff) | |
| parent | b096dac760b7d306c85e2b6b9b56779018596916 (diff) | |
| download | compcert-kvx-4dabb8cd9b292bb873155e02e430f79cb43dc629.tar.gz compcert-kvx-4dabb8cd9b292bb873155e02e430f79cb43dc629.zip | |
Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-work
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/Elab.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index f60e15a3..9e17cb7e 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2428,8 +2428,8 @@ let enter_typedef loc env sto (s, ty, init) = env end else begin - error loc "typedef redefinition with different types (%a vs %a)" - (print_typ env) ty (print_typ env) ty'; + error loc "redefinition of typedef '%s' with different type (%a vs %a)" + s (print_typ env) ty (print_typ env) ty'; env end | _ -> |