diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-04 22:17:45 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-04 22:17:45 +0200 |
commit | 8df444cbc4aa78d4effb03474b3709925ac7002a (patch) | |
tree | e251cf6733b0cf38ee125d649331687b829fe67a /cparser/Elab.ml | |
parent | 1b989dc9bff4a6425a929a5638362ca87edb122d (diff) | |
parent | 5493186b185143b8cea401fbbbf417d37ae7e665 (diff) | |
download | compcert-kvx-8df444cbc4aa78d4effb03474b3709925ac7002a.tar.gz compcert-kvx-8df444cbc4aa78d4effb03474b3709925ac7002a.zip |
Merge branch 'master' of github.com:AbsInt/CompCert
Diffstat (limited to 'cparser/Elab.ml')
-rw-r--r-- | cparser/Elab.ml | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index e81e6139..d1dce41f 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1786,13 +1786,21 @@ let enter_typedefs loc env sto dl = List.fold_left (fun env (s, ty, init) -> if init <> NO_INIT then error loc "initializer in typedef"; - if redef Env.lookup_typedef env s then - error loc "redefinition of typedef '%s'" s; - if redef Env.lookup_ident env s then - error loc "redefinition of identifier '%s' as different kind of symbol" s; - let (id, env') = Env.enter_typedef env s ty in - emit_elab env loc (Gtypedef(id, ty)); - env') env dl + match previous_def Env.lookup_typedef env s with + | Some (s',ty') -> + if equal_types env ty ty' then begin + warning loc "redefinition of typedef '%s'" s; + env + end else begin + error loc "redefinition of typedef '%s' with different type" s; + env + end + | None -> + if redef Env.lookup_ident env s then + error loc "redefinition of identifier '%s' as different kind of symbol" s; + let (id, env') = Env.enter_typedef env s ty in + emit_elab env loc (Gtypedef(id, ty)); + env') env dl let enter_or_refine_ident local loc env s sto ty = if redef Env.lookup_typedef env s then |