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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/funind/indfun.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index e10ed49ed..2ceda4f48 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -132,7 +132,7 @@ let rec abstract_glob_constr c = function let interp_casted_constr_with_implicits sigma env impls c = Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls - ~allow_patvar:false ~ltacvars:(Id.Set.empty, Id.Set.empty) c + ~allow_patvar:false ~ltacvars:(Id.Set.empty, Id.Set.empty,Id.Map.empty) c (* Construct a fixpoint as a Glob_term |