diff options
Diffstat (limited to 'pretyping/geninterp.ml')
| -rw-r--r-- | pretyping/geninterp.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/geninterp.ml b/pretyping/geninterp.ml index 1f8b926365..32152ad0e4 100644 --- a/pretyping/geninterp.ml +++ b/pretyping/geninterp.ml @@ -82,9 +82,10 @@ let register_val0 wit tag = (** Interpretation functions *) -type interp_sign = { - lfun : Val.t Id.Map.t; - extra : TacStore.t } +type interp_sign = + { lfun : Val.t Id.Map.t + ; poly : bool + ; extra : TacStore.t } type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t |