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/constrarg.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 'interp/constrarg.ml')
| -rw-r--r-- | interp/constrarg.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml index c25e02c02c..cb980f5a38 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -47,6 +47,8 @@ let wit_constr = unsafe_of_type ConstrArgType let wit_constr_may_eval = unsafe_of_type ConstrMayEvalArgType +let wit_uconstr = Genarg.make0 None "uconstr" + let wit_open_constr = unsafe_of_type OpenConstrArgType let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType @@ -65,4 +67,5 @@ let () = register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern"; register_name0 wit_tactic "Constrarg.wit_tactic"; register_name0 wit_sort "Constrarg.wit_sort"; + register_name0 wit_uconstr "Constrarg.uconstr"; register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl"; |