diff options
| author | Pierre-Marie Pédrot | 2019-10-10 16:50:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-18 10:29:09 +0200 |
| commit | 2dca6c1a3560522a11dd0afda8bd3c61d646ed2e (patch) | |
| tree | 9e0e729b46a86666eef26ee53a17735ecacf8fa6 /user-contrib/Ltac2/tac2env.mli | |
| parent | cc9856e33fa1a15fe699e8d9cd7b76086563683d (diff) | |
Allow to pass Ltac1 values to Ltac2 quotations.
This is the dual of #10344.
Diffstat (limited to 'user-contrib/Ltac2/tac2env.mli')
| -rw-r--r-- | user-contrib/Ltac2/tac2env.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli index 2dbb16e184..2f4a49a0f5 100644 --- a/user-contrib/Ltac2/tac2env.mli +++ b/user-contrib/Ltac2/tac2env.mli @@ -140,7 +140,7 @@ val ltac1_prefix : ModPath.t (** {5 Generic arguments} *) -val wit_ltac2 : (raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type +val wit_ltac2 : (Id.t CAst.t list * raw_tacexpr, Id.t list * glb_tacexpr, Util.Empty.t) genarg_type val wit_ltac2_quotation : (Id.t Loc.located, Id.t, Util.Empty.t) genarg_type (** {5 Helper functions} *) |