Some missing copyright headers.

a7ec0da6 · Robbert Krebbers · 1dee15b3 · a7ec0da6 · a7ec0da6
Commit a7ec0da6 authored 8 years ago by Robbert Krebbers
--- a/theories/functions.v
+++ b/theories/functions.v
+(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* This file is distributed under the terms of the BSD license. *)
 From stdpp Require Export base tactics.
 Set Default Proof Using "Type".


--- a/theories/hlist.v
+++ b/theories/hlist.v
+(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* This file is distributed under the terms of the BSD license. *)
 From stdpp Require Import tactics.
 Set Default Proof Using "Type".
 Local Set Universe Polymorphism.