diff options
| author | Pierre-Marie Pédrot | 2016-06-05 20:46:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-05 20:46:43 +0200 |
| commit | d5b059a28e07eda395510e1910636e7fdcf919ab (patch) | |
| tree | a9114a2aaa2d531dbab3a3d7797e19078f91157f /_tags | |
| parent | ba34fd27bd469ffde9977211bbd9d5b5fa9656b6 (diff) | |
| parent | 3ab71e34bf1f43e7e5e403ae7ff1e9d0dc9478e8 (diff) | |
Remove Q_constr from grammar folder.
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 |