From fb8142bb2fd84b10f4536fa63c972286365413f8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 Sep 2017 16:31:16 +0200
Subject: Export Ltac2.Notations in the Ltac2 entry module.

---
 theories/Ltac2.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Ltac2.v b/theories/Ltac2.v
index 996236325c..7b2f592ac6 100644
--- a/theories/Ltac2.v
+++ b/theories/Ltac2.v
@@ -18,4 +18,4 @@ Require Ltac2.Control.
 Require Ltac2.Fresh.
 Require Ltac2.Pattern.
 Require Ltac2.Std.
-Require Ltac2.Notations.
+Require Export Ltac2.Notations.
-- 
cgit v1.2.3