diff options
| author | Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org> | 2021-10-03 18:42:50 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-03 18:42:50 +0200 |
| commit | 990c96e18ca31781484f558d46c94537b5ec59cf (patch) | |
| tree | d4b610952733c6d2dfcf674cb289e74c1624f038 /MenhirLib/Validator_safe.v | |
| parent | a2a2529d78b86ece65cfc03fa8670538b85bc991 (diff) | |
| download | compcert-kvx-990c96e18ca31781484f558d46c94537b5ec59cf.tar.gz compcert-kvx-990c96e18ca31781484f558d46c94537b5ec59cf.zip | |
Synchronize vendored MenhirLib with upstream (#416)
It remains compatible with earlier Menhir versions.
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). |