diff options
Diffstat (limited to 'tactics/eqdecide.ml')
| -rw-r--r-- | tactics/eqdecide.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index d4cad3fa8..282b020ba 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -156,8 +156,9 @@ open Proofview.Notations (* spiwack: a PatternMatchingFailure wrapper around [Hipattern]. *) let match_eqdec sigma c = + Proofview.tclENV >>= fun env -> try - let (eqonleft,_,c1,c2,ty) = match_eqdec sigma c in + let (eqonleft,_,c1,c2,ty) = match_eqdec env sigma c in let (op,eq1,noteq,eq2) = match EConstr.kind sigma c with | App (op,[|ty1;ty2|]) -> |