diff options
Diffstat (limited to 'user-contrib/Ltac2/tac2env.ml')
| -rw-r--r-- | user-contrib/Ltac2/tac2env.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml index f6d07e484b..5479ba0d54 100644 --- a/user-contrib/Ltac2/tac2env.ml +++ b/user-contrib/Ltac2/tac2env.ml @@ -288,7 +288,8 @@ let ltac1_prefix = (** Generic arguments *) -let wit_ltac2 = Genarg.make0 "ltac2:value" +let wit_ltac2 = Genarg.make0 "ltac2:tactic" +let wit_ltac2_val = Genarg.make0 "ltac2:value" let wit_ltac2_constr = Genarg.make0 "ltac2:in-constr" let wit_ltac2_quotation = Genarg.make0 "ltac2:quotation" let () = Geninterp.register_val0 wit_ltac2 None |