diff options
Diffstat (limited to 'parsing/pcoq.ml4')
| -rw-r--r-- | parsing/pcoq.ml4 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 6792ae044..3b9708dc6 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -414,6 +414,8 @@ open Constr open Tactic open Vernac +(* current file and toplevel/vernac.ml *) + let define_quotation default s e = (if default then GEXTEND Gram |