From 900841d0bb4700fb2a3662457e7c4efea34a97e4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 18 Aug 2017 13:47:36 +0200
Subject: Exporting scopes for occurrences.

---
 src/tac2core.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/tac2core.ml')

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 *)
 
-- 
cgit v1.2.3