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 /tactics/tacsubst.ml | |
| 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 'tactics/tacsubst.ml')
| -rw-r--r-- | tactics/tacsubst.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 0d8923d5b..0872f8bbf 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -254,6 +254,7 @@ and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body) and subst_tacarg subst = function | Reference r -> Reference (subst_reference subst r) | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c) + | UConstr c -> UConstr (subst_glob_constr subst c) | MetaIdArg (_loc,_,_) -> assert false | TacCall (_loc,f,l) -> TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l) @@ -320,6 +321,7 @@ let () = Genintern.register_subst0 wit_intro_pattern (fun _ v -> v); Genintern.register_subst0 wit_tactic subst_tactic; Genintern.register_subst0 wit_sort (fun _ v -> v); - Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v) + Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v); + Genintern.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c) let _ = Hook.set Auto.extern_subst_tactic subst_tactic |