diff options
Diffstat (limited to 'user-contrib/Ltac2/tac2entries.mli')
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli index fed43a4dd5..4938e96cae 100644 --- a/user-contrib/Ltac2/tac2entries.mli +++ b/user-contrib/Ltac2/tac2entries.mli @@ -36,7 +36,7 @@ val perform_eval : pstate:Proof_global.t option -> raw_tacexpr -> unit (** {5 Notations} *) type scope_rule = -| ScopeRule : (raw_tacexpr, _, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule +| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.symbol * ('a -> raw_tacexpr) -> scope_rule type scope_interpretation = sexpr list -> scope_rule |