rename No_external_call to ._statement

src/semantics/FPBigStepClight.v

@@ -339,48 +339,48 @@ Qed.
 (** ===================================================== *)
 
 
-(** No_external_call st state that st doesn't have any direct external call
+(** No_external_call_statement st state that st doesn't have any direct external call
     e.i. there is no Sbuiltin.
     However, Scall are alowed and i don't know if they might have
     external call *)
-Inductive No_external_call : statement -> Prop :=
-  | NEC_Sskip : No_external_call Sskip
-  | NEC_Sassign : forall x v, No_external_call (Sassign x v)
-  | NEC_Sset : forall x v, No_external_call (Sset x v)
+Inductive No_external_call_statement : statement -> Prop :=
+  | NEC_Sskip : No_external_call_statement Sskip
+  | NEC_Sassign : forall x v, No_external_call_statement (Sassign x v)
+  | NEC_Sset : forall x v, No_external_call_statement (Sset x v)
   (** Scall might be dangerous ! *)
-  | NEC_Scall : forall i e le, No_external_call (Scall i e le)
+  | NEC_Scall : forall i e le, No_external_call_statement (Scall i e le)
   (** No Sbuiltin
     | NEC_Sbuiltin
   *)
   | NEC_Ssequence st1 st2 :
-      No_external_call st1 ->
-      No_external_call st2 ->
-        No_external_call (Ssequence st1 st2)
+      No_external_call_statement st1 ->
+      No_external_call_statement st2 ->
+        No_external_call_statement (Ssequence st1 st2)
   | NEC_Sifthenelse e st1 st2 :
-      No_external_call st1 ->
-      No_external_call st2 ->
-        No_external_call (Sifthenelse e st1 st2)
+      No_external_call_statement st1 ->
+      No_external_call_statement st2 ->
+        No_external_call_statement (Sifthenelse e st1 st2)
   | NEC_Sloop st1 st2 :
-      No_external_call st1 ->
-      No_external_call st2 ->
-        No_external_call (Sloop st1 st2)
-  | NEC_Sbreak : No_external_call Sbreak
-  | NEC_Scontinue : No_external_call Scontinue
-  | NEC_Sreturn : forall e, No_external_call (Sreturn e)
+      No_external_call_statement st1 ->
+      No_external_call_statement st2 ->
+        No_external_call_statement (Sloop st1 st2)
+  | NEC_Sbreak : No_external_call_statement Sbreak
+  | NEC_Scontinue : No_external_call_statement Scontinue
+  | NEC_Sreturn : forall e, No_external_call_statement (Sreturn e)
   | NEC_Sswitch : forall e lst, 
-      No_external_call_labeled lst ->
-        No_external_call (Sswitch e lst)
+      No_external_call_statement_labeled lst ->
+        No_external_call_statement (Sswitch e lst)
   | NEC_Slabel : forall l st,
-      No_external_call st ->
-        No_external_call (Slabel l st)
-  | NEC_Sgoto : forall l, No_external_call (Sgoto l)
+      No_external_call_statement st ->
+        No_external_call_statement (Slabel l st)
+  | NEC_Sgoto : forall l, No_external_call_statement (Sgoto l)
 
-with No_external_call_labeled : labeled_statements -> Type :=
-  | NECL_LSnil : No_external_call_labeled LSnil
+with No_external_call_statement_labeled : labeled_statements -> Prop :=
+  | NECL_LSnil : No_external_call_statement_labeled LSnil
   | NECL_LScons : forall l st lst, 
-      No_external_call st ->
-      No_external_call_labeled lst ->
-        No_external_call_labeled (LScons l st lst).
+      No_external_call_statement st ->
+      No_external_call_statement_labeled lst ->
+        No_external_call_statement_labeled (LScons l st lst).
 
 
 Axiom No_SBuiltin :