diff options
| author |  amblaf <you@example.com> | 2017-06-20 09:48:55 +0200 |
|---|---|---|
| committer | amblaf <you@example.com> | 2017-07-31 10:34:05 +0200 |
| commit | b84ab413f8434719dbbf5e09da9a0698b84b0106 (patch) | |
| tree | 5cbbc30806d595126f381518a8a0d83bc16394b4 /tactics/eqdecide.ml | |
| parent | 5c7d5fce3ed1de62ff5e1528a12adce0cdf2b0d9 (diff) | |
Replacing tclENV with the goal environment
In functions match_eqdec and check_unused_names
Diffstat (limited to 'tactics/eqdecide.ml')
| -rw-r--r-- | tactics/eqdecide.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 282b020ba..e16fcec7c 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -155,8 +155,7 @@ open Proofview.Notations (* spiwack: a PatternMatchingFailure wrapper around [Hipattern]. *) -let match_eqdec sigma c = - Proofview.tclENV >>= fun env -> +let match_eqdec env sigma c = try let (eqonleft,_,c1,c2,ty) = match_eqdec env sigma c in let (op,eq1,noteq,eq2) = @@ -203,8 +202,9 @@ let solveEqBranch rectype = begin Proofview.Goal.enter begin fun gl -> let concl = pf_concl gl in + let env = Proofview.Goal.env gl in let sigma = project gl in - match_eqdec sigma concl >>= fun (eqonleft,mk,lhs,rhs,_) -> + match_eqdec env sigma concl >>= fun (eqonleft,mk,lhs,rhs,_) -> let (mib,mip) = Global.lookup_inductive rectype in let nparams = mib.mind_nparams in let getargs l = List.skipn nparams (snd (decompose_app sigma l)) in @@ -230,8 +230,9 @@ let decideGralEquality = begin Proofview.Goal.enter begin fun gl -> let concl = pf_concl gl in + let env = Proofview.Goal.env gl in let sigma = project gl in - match_eqdec sigma concl >>= fun (eqonleft,mk,c1,c2,typ as data) -> + match_eqdec env sigma concl >>= fun (eqonleft,mk,c1,c2,typ as data) -> let headtyp = hd_app sigma (pf_compute gl typ) in begin match EConstr.kind sigma headtyp with | Ind (mi,_) -> Proofview.tclUNIT mi |