Merge branch 'named-structs'

- Switch CompCert C / Clight AST of composite types (structs and unions)
  from a structural representation to a nominal representation,
  closer to concrete syntax.
- This avoids algorithmic inefficiencies due to the structural representation.
- Closes PR#4.
- Smallstep: make small-step semantics more polymorphic in the type of the
  global environment.
- Globalenvs: introduce Senv.t (symbol environments) as a restricted view
  on Genv.t (full global environments).
- Events, Smallstep: use Senv instead of Genv to talk about global names.

1 files changed, 5 insertions, 5 deletions

diff --git a/common/Determinism.v b/common/Determinism.v
index 26a13ab2..d0099ba9 100644
--- a/common/Determinism.v
+++ b/common/Determinism.v
@@ -105,7 +105,7 @@ Proof.
 Qed.
 
 Lemma match_possible_traces:
-  forall (F V: Type) (ge: Genv.t F V) t1 t2 w0 w1 w2,
+  forall ge t1 t2 w0 w1 w2,
   match_traces ge t1 t2 -> possible_trace w0 t1 w1 -> possible_trace w0 t2 w2 ->
   t1 = t2 /\ w1 = w2.
 Proof.
@@ -508,14 +508,14 @@ Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
 Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
 Local Open Scope pair_scope.
 
-Definition world_sem : semantics := @Semantics
+Definition world_sem : semantics := @Semantics_gen
   (state L * world)%type
-  (funtype L)
-  (vartype L)
+  (genvtype L)
   (fun ge s t s' => step L ge s#1 t s'#1 /\ possible_trace s#2 t s'#2)
   (fun s => initial_state L s#1 /\ s#2 = initial_world)
   (fun s r => final_state L s#1 r)
-  (globalenv L).
+  (globalenv L)
+  (symbolenv L).
 
 (** If the original semantics is determinate, the world-aware semantics is deterministic. *)