diff options
| author | Maxime Dénès | 2019-04-05 12:18:49 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-10 15:41:45 +0200 |
| commit | 5af486406e366bf23558311a7367e573c617e078 (patch) | |
| tree | e2996582ca8eab104141dd75b82ac1777e53cb72 /plugins/extraction | |
| parent | f6dc8b19760aaf0cc14e6d9eb2d581ba1a05a762 (diff) | |
Remove calls to global env in Inductiveops
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extraction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index c9cfd74362..9db7c8d8d3 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -854,7 +854,7 @@ and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args = and extract_case env sg mle ((kn,i) as ip,c,br) mlt = (* [br]: bodies of each branch (in functional form) *) (* [ni]: number of arguments without parameters in each branch *) - let ni = constructors_nrealargs_env env ip in + let ni = constructors_nrealargs env ip in let br_size = Array.length br in assert (Int.equal (Array.length ni) br_size); if Int.equal br_size 0 then begin |