diff options
| author | Arnaud Spiwack | 2014-07-29 12:20:54 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-07-29 17:16:29 +0200 |
| commit | 52247f50fa9aed83cc4a9a714b6b8f779479fd9b (patch) | |
| tree | deba7d80c23fcef9ac3632beca3b0e0b7b8567bd /interp/constrintern.mli | |
| 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 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 1331fd968a..2b61c51dc9 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -67,7 +67,7 @@ val compute_internalization_env : env -> var_internalization_type -> Id.t list -> types list -> Impargs.manual_explicitation list list -> internalization_env -type ltac_sign = Id.Set.t * Id.Set.t +type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Id.Map.t type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) |