diff options
| author | Pierre-Marie Pédrot | 2016-06-04 16:25:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-05 19:27:03 +0200 |
| commit | 3ab71e34bf1f43e7e5e403ae7ff1e9d0dc9478e8 (patch) | |
| tree | a9114a2aaa2d531dbab3a3d7797e19078f91157f /_tags | |
| parent | 825d14e197f6dee1ed6b2c87f82be2d29b36ab97 (diff) | |
Removing the Q_constr file.
Diffstat (limited to '_tags')
| -rw-r--r-- | _tags | 2 |
1 files changed, 0 insertions, 2 deletions
@@ -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 |