diff options
Diffstat (limited to 'src/tac2quote.ml')
| -rw-r--r-- | src/tac2quote.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/tac2quote.ml b/src/tac2quote.ml index 3bddfe7594..5a26e7465c 100644 --- a/src/tac2quote.ml +++ b/src/tac2quote.ml @@ -22,6 +22,7 @@ let wit_ident = Arg.create "ident" let wit_constr = Arg.create "constr" let wit_open_constr = Arg.create "open_constr" let wit_ltac1 = Arg.create "ltac1" +let wit_ltac1val = Arg.create "ltac1val" (** Syntactic quoting of expressions. *) |