Commit 76fb6fa5 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump year in prelude copyright headers.

parent 939b747b
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on the option (** This file collects general purpose definitions and theorems on the option
data type that are not in the Coq standard library. *) data type that are not in the Coq standard library. *)
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** Properties about arbitrary pre-, partial, and total orders. We do not use (** Properties about arbitrary pre-, partial, and total orders. We do not use
the relation [⊆] because we often have multiple orders on the same structure *) the relation [⊆] because we often have multiple orders on the same structure *)
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This files implements an efficient implementation of finite maps whose keys (** This files implements an efficient implementation of finite maps whose keys
range over Coq's data type of positive binary naturals [positive]. The range over Coq's data type of positive binary naturals [positive]. The
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
From iris.prelude Require Export From iris.prelude Require Export
base base
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
From iris.prelude Require Export strings. From iris.prelude Require Export strings.
From iris.prelude Require Import relations. From iris.prelude Require Import relations.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file collects facts on proof irrelevant types/propositions. *) (** This file collects facts on proof irrelevant types/propositions. *)
From iris.prelude Require Export base. From iris.prelude Require Export base.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file collects definitions and theorems on abstract rewriting systems. (** This file collects definitions and theorems on abstract rewriting systems.
These are particularly useful as we define the operational semantics as a These are particularly useful as we define the operational semantics as a
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file implements sets as functions into Prop. *) (** This file implements sets as functions into Prop. *)
From iris.prelude Require Export collections. From iris.prelude Require Export collections.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** Merge sort. Adapted from the implementation of Hugo Herbelin in the Coq (** Merge sort. Adapted from the implementation of Hugo Herbelin in the Coq
standard library, but without using the module system. *) standard library, but without using the module system. *)
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
From iris.prelude Require Export tactics. From iris.prelude Require Export tactics.
Set Default Proof Using "Type". Set Default Proof Using "Type".
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This files implements an efficient implementation of finite maps whose keys (** This files implements an efficient implementation of finite maps whose keys
range over Coq's data type of strings [string]. The implementation uses radix-2 range over Coq's data type of strings [string]. The implementation uses radix-2
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
From Coq Require Import Ascii. From Coq Require Import Ascii.
From Coq Require Export String. From Coq Require Export String.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose tactics that are used throughout (** This file collects general purpose tactics that are used throughout
the development. *) the development. *)
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on vectors (** This file collects general purpose definitions and theorems on vectors
(lists of fixed length) and the fin type (bounded naturals). It uses the (lists of fixed length) and the fin type (bounded naturals). It uses the
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This files extends the implementation of finite over [positive] to finite (** This files extends the implementation of finite over [positive] to finite
maps whose keys range over Coq's data type of binary naturals [Z]. *) maps whose keys range over Coq's data type of binary naturals [Z]. *)
......
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