diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-17 19:24:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-21 19:36:38 +0100 |
| commit | b2beb9087628de23679a831e6273b91816f1ed27 (patch) | |
| tree | 40784a3be039885aef29c3c23fda2a0189fe2ac1 /pretyping/pretyping.mli | |
| parent | fcf425a4714f0c888b3d670a9a37fe52a6e49bc5 (diff) | |
Using dynamic values in tactic evaluation.
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index f8587d01c..8b76816ab 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -29,7 +29,7 @@ type typing_constraint = OfType of types | IsType | WithoutTypeConstraint type var_map = Pattern.constr_under_binders Id.Map.t type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t -type unbound_ltac_var_map = Genarg.tlevel Genarg.generic_argument Id.Map.t +type unbound_ltac_var_map = Genarg.Val.t Id.Map.t type ltac_var_map = { ltac_constrs : var_map; @@ -152,5 +152,5 @@ val interp_sort : evar_map -> glob_sort -> evar_map * sorts val interp_elimination_sort : glob_sort -> sorts_family val genarg_interp_hook : - (types -> env -> evar_map -> Genarg.typed_generic_argument Id.Map.t -> + (types -> env -> evar_map -> unbound_ltac_var_map -> Genarg.glob_generic_argument -> constr * evar_map) Hook.t |