From 3ab71e34bf1f43e7e5e403ae7ff1e9d0dc9478e8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 4 Jun 2016 16:25:16 +0200
Subject: Removing the Q_constr file.

---
 _tags | 2 --
 1 file changed, 2 deletions(-)

(limited to '_tags')

diff --git a/_tags b/_tags
index e8317d6148..9f77416a02 100644
--- a/_tags
+++ b/_tags
@@ -35,12 +35,10 @@
 "parsing/g_obligations.ml4": use_grammar
 
 "grammar/argextend.ml4": use_compat5b
-"grammar/q_constr.ml4": use_compat5b
 "grammar/tacextend.ml4": use_compat5b
 "grammar/vernacextend.ml4": use_compat5b
 
 <tactics/*.ml4>: use_grammar
-"tactics/hipattern.ml4": use_constr
 
 <plugins/**/*.ml4>: use_grammar
 "plugins/decl_mode/g_decl_mode.ml4": use_compat5
-- 
cgit v1.2.3