diff options
| author | Emilio Jesus Gallego Arias | 2019-02-13 05:37:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-27 23:56:18 +0100 |
| commit | c0cff3a7ebb79d1142090108c56e9aa64c3b481d (patch) | |
| tree | b316f32c8c5d879324031dd17ca317cb29ce4b1f /pretyping/geninterp.ml | |
| parent | 178672504f1c92b162c2575b14034cc7b698b6a4 (diff) | |
[geninterp] Track polymorphic status in tactic interpretation.
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 |