aboutsummaryrefslogtreecommitdiff
path: root/src/tac2core.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/tac2core.ml')
-rw-r--r--src/tac2core.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 72b4dbfe97..7539e1b697 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -893,6 +893,7 @@ let () = add_expr_scope "intropattern" Tac2entries.Pltac.q_intropattern
let () = add_expr_scope "intropatterns" Tac2entries.Pltac.q_intropatterns
let () = add_expr_scope "induction_clause" Tac2entries.Pltac.q_induction_clause
let () = add_expr_scope "rewriting" Tac2entries.Pltac.q_rewriting
+let () = add_expr_scope "clause" Tac2entries.Pltac.q_clause
let () = add_generic_scope "constr" Pcoq.Constr.constr Stdarg.wit_constr
let () = add_generic_scope "open_constr" Pcoq.Constr.constr Stdarg.wit_open_constr