diff options
Diffstat (limited to 'MenhirLib/Validator_complete.v')
| -rw-r--r-- | MenhirLib/Validator_complete.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/MenhirLib/Validator_complete.v b/MenhirLib/Validator_complete.v index ac4dd0c4..4b4d127a 100644 --- a/MenhirLib/Validator_complete.v +++ b/MenhirLib/Validator_complete.v @@ -22,12 +22,12 @@ Module Make(Import A:Automaton.T). (** We instantiate some sets/map. **) Module TerminalComparableM <: ComparableM. Definition t := terminal. - Instance tComparable : Comparable t := _. + Global Instance tComparable : Comparable t := _. End TerminalComparableM. Module TerminalOrderedType := OrderedType_from_ComparableM TerminalComparableM. Module StateProdPosComparableM <: ComparableM. Definition t := (state*production*nat)%type. - Instance tComparable : Comparable t := _. + Global Instance tComparable : Comparable t := _. End StateProdPosComparableM. Module StateProdPosOrderedType := OrderedType_from_ComparableM StateProdPosComparableM. @@ -117,7 +117,7 @@ Definition forallb_items items_map (P:state -> production -> nat -> TerminalSet. (** Typeclass instances for synthetizing the validator. *) -Instance is_validator_subset S1 S2 : +Global Instance is_validator_subset S1 S2 : IsValidator (TerminalSet.Subset S1 S2) (TerminalSet.subset S1 S2). Proof. intros ?. by apply TerminalSet.subset_2. Qed. @@ -150,7 +150,7 @@ Global Hint Extern 2 (IsValidator (state_has_future _ _ _ _) _) => validator. This instance is used for [non_terminal_closed]. *) -Instance is_validator_forall_lookahead_set lset P b: +Global Instance is_validator_forall_lookahead_set lset P b: (forall lookahead, TerminalSet.In lookahead lset -> IsValidator (P lookahead) b) -> IsValidator (forall lookahead, TerminalSet.In lookahead lset -> P lookahead) b. Proof. unfold IsValidator. firstorder. Qed. @@ -237,7 +237,7 @@ Proof. eapply Hval2 with (pos := pos); eauto; []. revert EQ. unfold future_of_prod=>-> //. Qed. -(* We need a hint for expplicitely instantiating b1 and b2 with lambdas. *) +(* We need a hint to explicitly instantiate b1 and b2 with lambdas. *) Global Hint Extern 0 (IsValidator (forall st prod fut lookahead, state_has_future st prod fut lookahead -> _) @@ -247,7 +247,7 @@ Global Hint Extern 0 (IsValidator : typeclass_instances. (* Used in [start_future] only. *) -Instance is_validator_forall_state_has_future im st prod : +Global Instance is_validator_forall_state_has_future im st prod : IsItemsMap im -> IsValidator (forall look, state_has_future st prod (rev' (prod_rhs_rev prod)) look) |