Commit 5138e988 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

coq-menhirlib : use -R and drop "From MenhirLib"

parent 3f218a9a
Pipeline #65021 passed with stages
in 22 seconds
......@@ -12,8 +12,8 @@
(* *)
(* *********************************************************************)
From MenhirLib Require Grammar.
From MenhirLib Require Export Alphabet.
Require Grammar.
Require Export Alphabet.
From Coq Require Import Orders.
From Coq Require Export List Syntax.
......
......@@ -13,7 +13,7 @@
(* *********************************************************************)
From Coq Require Import List Syntax Orders.
From MenhirLib Require Import Alphabet.
Require Import Alphabet.
(** The terminal non-terminal alphabets of the grammar. **)
Module Type Alphs.
......
......@@ -14,9 +14,8 @@
From Coq Require Import Streams List Syntax.
From Coq.ssr Require Import ssreflect.
From MenhirLib Require Automaton.
From MenhirLib Require Import Alphabet Grammar.
From MenhirLib Require Import Validator_safe.
Require Automaton.
Require Import Alphabet Grammar Validator_safe.
Module Make(Import A:Automaton.T).
Module Import ValidSafe := Validator_safe.Make A.
......
......@@ -14,8 +14,8 @@
From Coq Require Import Streams List Syntax Arith.
From Coq.ssr Require Import ssreflect.
From MenhirLib Require Import Alphabet Grammar.
From MenhirLib Require Automaton Interpreter Validator_complete.
Require Import Alphabet Grammar.
Require Automaton Interpreter Validator_complete.
Module Make(Import A:Automaton.T) (Import Inter:Interpreter.T A).
Module Import Valid := Validator_complete.Make A.
......
......@@ -13,8 +13,8 @@
(* *********************************************************************)
From Coq Require Import Streams List Syntax.
From MenhirLib Require Import Alphabet.
From MenhirLib Require Grammar Automaton Interpreter.
Require Import Alphabet.
Require Grammar Automaton Interpreter.
From Coq.ssr Require Import ssreflect.
Module Make(Import A:Automaton.T) (Import Inter:Interpreter.T A).
......
......@@ -12,7 +12,7 @@
(* *)
(* *********************************************************************)
From MenhirLib Require Grammar Automaton Interpreter_correct Interpreter_complete.
Require Grammar Automaton Interpreter_correct Interpreter_complete.
From Coq Require Import Syntax.
Module Make(Export Aut:Automaton.T).
......
PWD := $(shell pwd)
COQINCLUDE := \
-Q $(PWD) MenhirLib \
COQINCLUDE := -R $(PWD) MenhirLib \
export
......
......@@ -13,8 +13,8 @@
(* *********************************************************************)
From Coq Require Import List Syntax.
From MenhirLib Require Automaton.
From MenhirLib Require Import Alphabet.
Require Automaton.
Require Import Alphabet.
Module Make(Import A:Automaton.T).
......
......@@ -13,8 +13,8 @@
(* *********************************************************************)
From Coq Require Import List Syntax.
From MenhirLib Require Automaton.
From MenhirLib Require Import Alphabet.
Require Automaton.
Require Import Alphabet.
Module Make(Import A:Automaton.T).
......
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