diff options
| author | William Lawvere | 2017-06-13 22:22:36 -0700 |
|---|---|---|
| committer | William Lawvere | 2017-06-13 22:22:36 -0700 |
| commit | af39f62ad21f71a860e287e4d217b24dc9e2106b (patch) | |
| tree | 43c14ae184f24fffaf495dade6d27a1c2fac3e1a /plugins/extraction/mlutil.mli | |
| parent | 3b0830ce0233db5b612e0b5bb92e89fa644eb0e4 (diff) | |
| parent | 7e63c300a3aa1e3befb29bab9094e8b1939824bb (diff) | |
Merge remote-tracking branch 'upstream/trunk' into trunk
Diffstat (limited to 'plugins/extraction/mlutil.mli')
| -rw-r--r-- | plugins/extraction/mlutil.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 2655dfc897..6924dc9ffe 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -49,7 +49,7 @@ end (*s Utility functions over ML types without meta *) -val type_mem_kn : mutual_inductive -> ml_type -> bool +val type_mem_kn : MutInd.t -> ml_type -> bool val type_maxvar : ml_type -> int |