diff options
| author |  amblaf <you@example.com> | 2017-06-15 11:34:40 +0200 |
|---|---|---|
| committer | amblaf <you@example.com> | 2017-07-31 10:34:00 +0200 |
| commit | 7a56397ae26854df6335a3325353d0a5d6c894ea (patch) | |
| tree | 76b60550d291123d47497196e963dff7e2589498 /tactics/eqdecide.ml | |
| parent | 17f37f42792b3150fcebb6236b9896845957b89d (diff) | |
Remove references to Global.env in tactics/*.ml
Only in ml files that are not related to Coq commands
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|]) -> |