aboutsummaryrefslogtreecommitdiff
path: root/src/tac2core.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/tac2core.ml')
-rw-r--r--src/tac2core.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml
index b8e50ad1df..3ce2ed53a8 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -919,10 +919,12 @@ 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_expr_scope "occurrences" Tac2entries.Pltac.q_occurrences
let () = add_expr_scope "dispatch" Tac2entries.Pltac.q_dispatch
let () = add_generic_scope "constr" Pcoq.Constr.constr Stdarg.wit_constr
let () = add_generic_scope "open_constr" Pcoq.Constr.constr Stdarg.wit_open_constr
+let () = add_generic_scope "pattern" Pcoq.Constr.constr wit_pattern
(** seq scope, a bit hairy *)