From a7ec0da6203a1f602218f2ad7007b3f68934c566 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Mar 2017 15:58:56 +0100
Subject: [PATCH] Some missing copyright headers.

---
 theories/functions.v | 2 ++
 theories/hlist.v     | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/theories/functions.v b/theories/functions.v
index 868a430b..cbf5cd3c 100644
--- a/theories/functions.v
+++ b/theories/functions.v
@@ -1,3 +1,5 @@
+(* 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".
 
diff --git a/theories/hlist.v b/theories/hlist.v
index 7c0dff7f..e36296e6 100644
--- a/theories/hlist.v
+++ b/theories/hlist.v
@@ -1,3 +1,5 @@
+(* 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.
-- 
GitLab