Commit 1eaae61e authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Headache, licences, headers for coq-menhirlib.

parent 61e48315
Pipeline #65048 passed with stages
in 21 seconds
......@@ -82,10 +82,12 @@ MENHIRLIB_FILES := $(shell for m in $(MENHIRLIB_MODULES) ; do \
# in MenhirLib carry the "library" license, while every other file
# carries the "regular" license.
HEADACHE := headache
SRCHEAD := $(CURRENT)/headers/regular-header
LIBHEAD := $(CURRENT)/headers/library-header
FIND := $(shell if command -v gfind >/dev/null ; then echo gfind ; else echo find ; fi)
HEADACHE := headache
SRCHEAD := $(CURRENT)/headers/regular-header
LIBHEAD := $(CURRENT)/headers/library-header
COQLIBHEAD := $(CURRENT)/headers/coq-library-header
HEADACHECOQCONF := $(CURRENT)/headers/headache-coq.conf
FIND := $(shell if command -v gfind >/dev/null ; then echo gfind ; else echo find ; fi)
.PHONY: headache
headache:
......@@ -94,6 +96,9 @@ headache:
@ for file in src/standard.mly $(MENHIRLIB_FILES) ; do \
$(HEADACHE) -h $(LIBHEAD) $$file ; \
done
@ for file in coq-menhirlib/src/*.v ; do \
$(HEADACHE) -h $(COQLIBHEAD) -c $(HEADACHECOQCONF) $$file ; \
done
# -------------------------------------------------------------------------
......
......@@ -5,8 +5,13 @@ In the following, "THE LIBRARY" refers to the following files:
2- the OCaml source files whose basename appears in the file
src/menhirLib.mlpack and whose extension is ".ml" or ".mli".
"THE GENERATOR" refers to all other files in this archive or repository,
except those in the subdirectory test/, which are not covered by this license.
"THE COQ LIBRARY" refers to the files in the subdirectory
coq-menhirlib/.
"THE GENERATOR" refers to the files of this archive which are neither
part of THE LIBRARY, nor part of THE COQ LIBRARY, nor in the
subdirectory test/. Files in the subdirectory test/ are not covered
by this license.
THE GENERATOR is distributed under the terms of the GNU General Public
License version 2 (included below).
......@@ -14,6 +19,12 @@ License version 2 (included below).
THE LIBRARY is distributed under the terms of the GNU Library General
Public License version 2 (included below).
THE COQ LIBRARY is distributed under the terms of the GNU Lesser
General Public License as published by the Free Software Foundation,
either version 3 of the License, or (at your option) any later
version. Version 3 of the GNU Lesser General Public License is
included in the file coq-menhirlib/LICENSE.
As a special exception to the GNU Library General Public License, you
may link, statically or dynamically, a "work that uses the Library"
with a publicly distributed version of the Library to produce an
......
This diff is collapsed.
(* *********************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 3 of *)
(* the License, or (at your option) any later version. *)
(* *)
(* *********************************************************************)
(****************************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under *)
(* the terms of the GNU Lesser General Public License as published by the *)
(* Free Software Foundation, either version 3 of the License, or (at your *)
(* option) any later version, as described in the file LICENSE. *)
(* *)
(****************************************************************************)
From Coq Require Import Omega List Syntax Relations RelationClasses.
......
(* *********************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 3 of *)
(* the License, or (at your option) any later version. *)
(* *)
(* *********************************************************************)
(****************************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under *)
(* the terms of the GNU Lesser General Public License as published by the *)
(* Free Software Foundation, either version 3 of the License, or (at your *)
(* option) any later version, as described in the file LICENSE. *)
(* *)
(****************************************************************************)
Require Grammar.
Require Export Alphabet.
......
(* *********************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 3 of *)
(* the License, or (at your option) any later version. *)
(* *)
(* *********************************************************************)
(****************************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under *)
(* the terms of the GNU Lesser General Public License as published by the *)
(* Free Software Foundation, either version 3 of the License, or (at your *)
(* option) any later version, as described in the file LICENSE. *)
(* *)
(****************************************************************************)
From Coq Require Import List Syntax Orders.
Require Import Alphabet.
......
(* *********************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 3 of *)
(* the License, or (at your option) any later version. *)
(* *)
(* *********************************************************************)
(****************************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under *)
(* the terms of the GNU Lesser General Public License as published by the *)
(* Free Software Foundation, either version 3 of the License, or (at your *)
(* option) any later version, as described in the file LICENSE. *)
(* *)
(****************************************************************************)
From Coq Require Import Streams List Syntax.
From Coq.ssr Require Import ssreflect.
......
(* *********************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 3 of *)
(* the License, or (at your option) any later version. *)
(* *)
(* *********************************************************************)
(****************************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under *)
(* the terms of the GNU Lesser General Public License as published by the *)
(* Free Software Foundation, either version 3 of the License, or (at your *)
(* option) any later version, as described in the file LICENSE. *)
(* *)
(****************************************************************************)
From Coq Require Import Streams List Syntax Arith.
From Coq.ssr Require Import ssreflect.
......
(* *********************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 3 of *)
(* the License, or (at your option) any later version. *)
(* *)
(* *********************************************************************)
(****************************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under *)
(* the terms of the GNU Lesser General Public License as published by the *)
(* Free Software Foundation, either version 3 of the License, or (at your *)
(* option) any later version, as described in the file LICENSE. *)
(* *)
(****************************************************************************)
From Coq Require Import Streams List Syntax.
Require Import Alphabet.
......
(* *********************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 3 of *)
(* the License, or (at your option) any later version. *)
(* *)
(* *********************************************************************)
(****************************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under *)
(* the terms of the GNU Lesser General Public License as published by the *)
(* Free Software Foundation, either version 3 of the License, or (at your *)
(* option) any later version, as described in the file LICENSE. *)
(* *)
(****************************************************************************)
Require Grammar Automaton Interpreter_correct Interpreter_complete.
From Coq Require Import Syntax.
......
(* *********************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 3 of *)
(* the License, or (at your option) any later version. *)
(* *)
(* *********************************************************************)
(****************************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under *)
(* the terms of the GNU Lesser General Public License as published by the *)
(* Free Software Foundation, either version 3 of the License, or (at your *)
(* option) any later version, as described in the file LICENSE. *)
(* *)
(****************************************************************************)
From Coq Require Import List Syntax.
Require Automaton.
......
(* *********************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 3 of *)
(* the License, or (at your option) any later version. *)
(* *)
(* *********************************************************************)
(****************************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under *)
(* the terms of the GNU Lesser General Public License as published by the *)
(* Free Software Foundation, either version 3 of the License, or (at your *)
(* option) any later version, as described in the file LICENSE. *)
(* *)
(****************************************************************************)
From Coq Require Import List Syntax.
Require Automaton.
......
(****************************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under *)
(* the terms of the GNU Lesser General Public License as published by the *)
(* Free Software Foundation, either version 3 of the License, or (at your *)
(* option) any later version, as described in the file LICENSE. *)
(* *)
(****************************************************************************)
Definition require_unreleased := tt.
Menhir
Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud
Copyright Inria. All rights reserved. This file is distributed under
the terms of the GNU Lesser General Public License as published by the
Free Software Foundation, either version 3 of the License, or (at your
option) any later version, as described in the file LICENSE.
".*\\.v" -> frame open:"(*" line:"*" close:"*)"
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