Improve semantics definition

src/semantics/FPBigStep.v

@@ -273,6 +273,6 @@ Module FP_BIGSTEP (EVAL_Def: EVAL_ENV)
   End FlightPlan.
 
   Definition semantics_fp (fp: flight_plan): fp_semantics := 
-    FP_Semantics_gen fp_env ((step_prop step) fp) (initial_env fp).
+    FP_Semantics_gen ((step_prop step) fp) (initial_env fp).
 
 End FP_BIGSTEP.

src/semantics/FPBigStepClight.v

@@ -56,7 +56,7 @@ Module C_BIGSTEP.
 
   Definition semantics_fpc (prog: program): fp_semantics :=
     let ge: genv := Clight.globalenv prog in
-    FP_Semantics_gen fp_cenv (step ge) (initial_state prog).
+    FP_Semantics_gen (step ge) (initial_state prog).
 
 (** * Proof that step is deterministic *)
 

src/semantics/FPBigStepExtended.v

@@ -558,6 +558,6 @@ Module FPE_BIGSTEP (EVAL_Def: EVAL_ENV)
     initial_env (` fp) e.
 
   Definition semantics_fpe (fp: flight_plan_wf) : fp_semantics := 
-    FP_Semantics_gen fp_env ((step_prop step) fp) (initial_env_wf fp).
+    FP_Semantics_gen ((step_prop step) fp) (initial_env_wf fp).
 
 End FPE_BIGSTEP.

src/semantics/FPBigStepGeneric.v

@@ -30,8 +30,6 @@ Set Implicit Arguments.
 (** Definition of a semantics *)
 
 Record fp_semantics: Type := FP_Semantics_gen {
-  (** Type of the flight plan *)
-  flight_plan_type: Type;
   (** Environment for the semantics *)
   env: Type;
   (** Properties stating a step for the semantics *)

src/semantics/FPBigStepSized.v

@@ -1072,7 +1072,7 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
     step fps e = e'.
  
   Definition semantics_fps (fp: flight_plan_sized): fp_semantics := 
-    FP_Semantics_gen fp_env8 (step_size fp) (init_env8_prop fp).
+    FP_Semantics_gen (step_size fp) (init_env8_prop fp).
 
   (** Definition of an induction principle *)
   Lemma run_step_ind8: