diff options
Diffstat (limited to 'MenhirLib/Validator_safe.v')
| -rw-r--r-- | MenhirLib/Validator_safe.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/MenhirLib/Validator_safe.v b/MenhirLib/Validator_safe.v index e7a54b47..0f32ea50 100644 --- a/MenhirLib/Validator_safe.v +++ b/MenhirLib/Validator_safe.v @@ -62,7 +62,7 @@ Fixpoint is_prefix (l1 l2:list symbol) := | _::_, [] => false end. -Instance prefix_is_validator l1 l2 : IsValidator (prefix l1 l2) (is_prefix l1 l2). +Global Instance prefix_is_validator l1 l2 : IsValidator (prefix l1 l2) (is_prefix l1 l2). Proof. revert l2. induction l1 as [|x1 l1 IH]=>l2 Hpref. - constructor. @@ -127,7 +127,7 @@ Fixpoint is_prefix_pred (l1 l2:list (state->bool)) := | _::_, [] => false end. -Instance prefix_pred_is_validator l1 l2 : +Global Instance prefix_pred_is_validator l1 l2 : IsValidator (prefix_pred l1 l2) (is_prefix_pred l1 l2). Proof. revert l2. induction l1 as [|x1 l1 IH]=>l2 Hpref. @@ -180,7 +180,7 @@ Fixpoint is_state_valid_after_pop (state:state) (to_pop:list symbol) annot := | p::pl, s::sl => is_state_valid_after_pop state sl pl end. -Instance impl_is_state_valid_after_pop_is_validator state sl pl P b : +Global Instance impl_is_state_valid_after_pop_is_validator state sl pl P b : IsValidator P b -> IsValidator (state_valid_after_pop state sl pl -> P) (if is_state_valid_after_pop state sl pl then b else true). |