diff options
| author | Gaëtan Gilbert | 2020-08-27 11:12:14 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-09-30 11:37:03 +0200 |
| commit | 0fa5751429e92f6555e9cbe3e3509fec658b879c (patch) | |
| tree | 4993e6fdc0714e8f353a421e56709e89f52af27b /vernac | |
| parent | 2c802aaf74c83274ae922c59081c01bfc267d31b (diff) | |
interp_context_evars: removed unused [shift] argument
Became unused in e034b4090ca45410853db60ae2a5d2f220b48792
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comFixpoint.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 564d24c1ea..78572c6aa6 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -110,7 +110,7 @@ let interp_fix_context ~program_mode ~cofix env sigma fix = else [], fix.Vernacexpr.binders in let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma before in let sigma, (impl_env', ((env'', ctx'), imps')) = - interp_context_evars ~program_mode ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after + interp_context_evars ~program_mode ~impl_env env' sigma after in let annot = Option.map (fun _ -> List.length (Termops.assums_of_rel_context ctx)) fix.Vernacexpr.rec_order in sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot) |