From e39b5b8eaa89950216bca646b5e9ef9b56bea7be Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Jun 2015 14:19:31 +0200
Subject: Code documentation of the TACTIC/VERNAC EXTEND macros.

---
 grammar/tacextend.ml4    | 2 ++
 grammar/vernacextend.ml4 | 2 ++
 2 files changed, 4 insertions(+)

(limited to 'grammar')

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index f5f11e30a8..66f82fcdfc 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "tools/compat5b.cmo" i*)
 
+(** Implementation of the TACTIC EXTEND macro. *)
+
 open Util
 open Pp
 open Names
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 9db89308fb..03061d8bde 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "tools/compat5b.cmo" i*)
 
+(** Implementation of the VERNAC EXTEND macro. *)
+
 open Pp
 open Util
 open Q_util
-- 
cgit v1.2.3