diff options
| author | coqbot-app[bot] | 2020-10-01 17:55:45 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-01 17:55:45 +0000 |
| commit | b842e83ce941c995dfb266eee33c73e565785554 (patch) | |
| tree | d7e90d993517f1ed5b4659880ecb0e12fa9a6c79 /vernac | |
| parent | 7ffb5e663784fffb2cd6aae87bc38a5dc2f37710 (diff) | |
| parent | 0fa5751429e92f6555e9cbe3e3509fec658b879c (diff) | |
Merge PR #13116: interp_context_evars: removed unused [shift] argument
Reviewed-by: ejgallego
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) |