diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-07-29 12:20:54 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-07-29 17:16:29 +0200 |
| commit | 52247f50fa9aed83cc4a9a714b6b8f779479fd9b (patch) | |
| tree | deba7d80c23fcef9ac3632beca3b0e0b7b8567bd /intf | |
| parent | dfb5897b99cd21934c5d096c329585367665b986 (diff) | |
Add a type of untyped term to Ltac's value.
It is meant to avoid intermediary retyping when a term is built in Ltac. See #3218.
The implementation makes a small modification in Constrintern: now the main internalisation function can take an extra substitution from Ltac variables to glob_constr and will apply the substitution during the internalisation.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 1375552c3..99e151e38 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -174,6 +174,10 @@ and ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg = | TacGeneric of 'lev generic_argument | MetaIdArg of Loc.t * bool * string | ConstrMayEval of ('trm,'cst,'pat) may_eval + | UConstr of 'trm (* We can reuse ['trm] because terms and untyped terms + only differ at interpretation time (and not at + internalisation), and the output of interpration + is not a variant of [tactic_expr]. *) | Reference of 'ref | TacCall of Loc.t * 'ref * ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg list |