diff options
| author | Maxime Dénès | 2019-04-04 18:17:57 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-10 15:41:43 +0200 |
| commit | 3b980d937b5adfbae472ed8a13748a451fdf3450 (patch) | |
| tree | a3a2fcc4273df543218dbde93a5a5a4934fb0fea /plugins/ssr/ssrelim.ml | |
| parent | 8fe32139aeb965b056c0d1e9c8fab2324dbb7ba6 (diff) | |
Remove calls to global env from indrec
Diffstat (limited to 'plugins/ssr/ssrelim.ml')
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 350bb9019e..675e4d2457 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -194,7 +194,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let sort = Tacticals.elimination_sort_of_goal gl in let gl, elim = if not is_case then - let t,gl= pf_fresh_global (Indrec.lookup_eliminator (kn,i) sort) gl in + let t,gl= pf_fresh_global (Indrec.lookup_eliminator env (kn,i) sort) gl in gl, t else Tacmach.pf_eapply (fun env sigma () -> |