From e73d5db97cdb22cce2ee479469f62af3c4b6264a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 8 Jul 2016 14:43:57 +0200 Subject: Port to Coq 8.5pl2 Manual merging of branch jhjourdan:coq8.5. No other change un functionality. --- cparser/validator/Interpreter_safe.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'cparser/validator/Interpreter_safe.v') 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. -- cgit