diff options
Diffstat (limited to 'src/tac2entries.mli')
| -rw-r--r-- | src/tac2entries.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/tac2entries.mli b/src/tac2entries.mli index 0dd1d5a113..cf6cdfa74b 100644 --- a/src/tac2entries.mli +++ b/src/tac2entries.mli @@ -65,4 +65,5 @@ val q_induction_clause : raw_tacexpr Pcoq.Gram.entry val q_rewriting : raw_tacexpr Pcoq.Gram.entry val q_clause : raw_tacexpr Pcoq.Gram.entry val q_dispatch : raw_tacexpr Pcoq.Gram.entry +val q_occurrences : raw_tacexpr Pcoq.Gram.entry end |