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 /tactics/equality.ml | |
| parent | 8fe32139aeb965b056c0d1e9c8fab2324dbb7ba6 (diff) | |
Remove calls to global env from indrec
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 412fbbfd1b..d5fdad0127 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -356,7 +356,7 @@ let find_elim hdcncl lft2rgt dep cls ot = match EConstr.kind sigma hdcncl with | Ind (ind_sp,u) -> let pr1 = - lookup_eliminator ind_sp (elimination_sort_of_clause cls gl) + lookup_eliminator env ind_sp (elimination_sort_of_clause cls gl) in begin match lft2rgt, cls with | Some true, None |