diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-07-08 14:43:57 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-07-08 14:43:57 +0200 |
| commit | e73d5db97cdb22cce2ee479469f62af3c4b6264a (patch) | |
| tree | 035d31018c2abec698eb49a205c60bbf5c24ba0d /cparser/validator/Interpreter_safe.v | |
| parent | db2445b3b745abd1a26f5a832a29ca269c725277 (diff) | |
| download | compcert-e73d5db97cdb22cce2ee479469f62af3c4b6264a.tar.gz compcert-e73d5db97cdb22cce2ee479469f62af3c4b6264a.zip | |
Port to Coq 8.5pl2
Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
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. |