From 990c96e18ca31781484f558d46c94537b5ec59cf Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan Date: Sun, 3 Oct 2021 18:42:50 +0200 Subject: Synchronize vendored MenhirLib with upstream (#416) It remains compatible with earlier Menhir versions. --- MenhirLib/Validator_safe.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'MenhirLib/Validator_safe.v') 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). -- cgit