diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-11 08:30:14 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-11 08:30:14 +0200 |
commit | d5b86a98560c36fbcb3ab8d2698e09147acda512 (patch) | |
tree | f3ab850a1620fa5d3dbbe439998d09de8e0d817d /cparser/validator/Interpreter_safe.v | |
parent | ea2d6b70ed06c60dba9ba81cf53883c85fb92068 (diff) | |
parent | 3872ce9f9806d9af334b1fde092145edf664d170 (diff) | |
download | compcert-d5b86a98560c36fbcb3ab8d2698e09147acda512.tar.gz compcert-d5b86a98560c36fbcb3ab8d2698e09147acda512.zip |
Merge branch 'master' into add-file
Diffstat (limited to 'cparser/validator/Interpreter_safe.v')
-rw-r--r-- | cparser/validator/Interpreter_safe.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/cparser/validator/Interpreter_safe.v b/cparser/validator/Interpreter_safe.v index f094ddce..a1aa35b8 100644 --- a/cparser/validator/Interpreter_safe.v +++ b/cparser/validator/Interpreter_safe.v @@ -69,15 +69,15 @@ Inductive stack_invariant: stack -> Prop := (symb_stack_of_stack stack) -> prefix_pred (head_states_of_state (state_of_stack init stack)) (state_stack_of_stack stack) -> - stack_invariant_rec stack -> + stack_invariant_next stack -> stack_invariant stack -with stack_invariant_rec: stack -> Prop := - | stack_invariant_rec_nil: - stack_invariant_rec [] - | stack_invariant_rec_cons: +with stack_invariant_next: stack -> Prop := + | stack_invariant_next_nil: + stack_invariant_next [] + | stack_invariant_next_cons: forall state_cur st stack_rec, stack_invariant stack_rec -> - stack_invariant_rec (existT _ state_cur st::stack_rec). + stack_invariant_next (existT _ state_cur st::stack_rec). (** [pop] conserves the stack invariant and does not crash under the assumption that we can pop at this place. |