Commit 53f94fa4 authored by Antonio Nikishaev's avatar Antonio Nikishaev Committed by Jacques-Henri Jourdan

use ListNotations explicitly

parent a9e7fc51
Pipeline #141807 passed with stages
in 24 seconds
......@@ -11,7 +11,8 @@
(* *)
(****************************************************************************)
From Coq Require Import Omega List Syntax Relations RelationClasses.
From Coq Require Import Omega List Relations RelationClasses.
Import ListNotations.
Local Obligation Tactic := intros.
......
......@@ -11,7 +11,8 @@
(* *)
(****************************************************************************)
From Coq Require Import List Syntax Orders.
From Coq Require Import List Orders.
Import ListNotations.
Require Import Alphabet.
(** The terminal non-terminal alphabets of the grammar. **)
......
......@@ -12,6 +12,7 @@
(****************************************************************************)
From Coq Require Import List Syntax.
Import ListNotations.
From Coq.ssr Require Import ssreflect.
Require Automaton.
Require Import Alphabet Grammar Validator_safe.
......@@ -82,6 +83,7 @@ Proof. by rewrite /cast -Eqdep_dec.eq_rect_eq_dec. Qed.
CoInductive buffer : Type :=
Buf_cons { buf_head : token; buf_tail : buffer }.
Declare Scope buffer_scope.
Delimit Scope buffer_scope with buf.
Bind Scope buffer_scope with buffer.
......
......@@ -11,7 +11,8 @@
(* *)
(****************************************************************************)
From Coq Require Import List Syntax Arith.
From Coq Require Import List Arith.
Import ListNotations.
From Coq.ssr Require Import ssreflect.
Require Import Alphabet Grammar.
Require Automaton Interpreter Validator_complete.
......
......@@ -11,7 +11,8 @@
(* *)
(****************************************************************************)
From Coq Require Import List Syntax.
From Coq Require Import List.
Import ListNotations.
Require Import Alphabet.
Require Grammar Automaton Interpreter.
From Coq.ssr Require Import ssreflect.
......
......@@ -13,6 +13,7 @@
From Coq Require Import List Syntax Derive.
From Coq.ssr Require Import ssreflect.
Import ListNotations.
Require Automaton.
Require Import Alphabet Validator_classes.
......
......@@ -12,6 +12,7 @@
(****************************************************************************)
From Coq Require Import List Syntax Derive.
Import ListNotations.
From Coq.ssr Require Import ssreflect.
Require Automaton.
Require Import Alphabet Validator_classes.
......
Require Import Parser Lexer List String PeanoNat.
Import MenhirLibParser.Inter.
Import ListNotations.
Open Scope string_scope.
(** Lexer + Parser for little arithmetic expressions *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment