diff --git a/theories/functions.v b/theories/functions.v
index 868a430b336e13894adca08da2b4b6c598c34159..cbf5cd3c94f4b89924cc2016b4912a11a46ce751 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 7c0dff7fca533278e18f4c4ee889b18bb817a800..e36296e60cbd24c02277b91056e08ee3497ede13 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.