diff options
Diffstat (limited to 'tactics/geninterp.mli')
| -rw-r--r-- | tactics/geninterp.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/geninterp.mli b/tactics/geninterp.mli index 0f5e6bf0ff..c3d7048354 100644 --- a/tactics/geninterp.mli +++ b/tactics/geninterp.mli @@ -14,7 +14,7 @@ open Genarg module TacStore : Store.S type interp_sign = { - lfun : (Id.t * tlevel generic_argument) list; + lfun : tlevel generic_argument Id.Map.t; extra : TacStore.t } type ('glb, 'top) interp_fun = interp_sign -> |