diff options
| author | Arnaud Spiwack | 2014-02-25 12:32:34 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-02-25 17:13:45 +0100 |
| commit | f931b170b3be3da2e2c245c566aad2b483223a51 (patch) | |
| tree | 530aa41e9827f30a01248820d0eef577901470de | |
| parent | d35a5022f45f1082c83891a6d0af32485a9db7d6 (diff) | |
Tacinterp: remove unnecessary return/bind pairs.
| -rw-r--r-- | tactics/tacinterp.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a8180f4929..3dd42e0e54 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1994,12 +1994,14 @@ and interp_atomic ist tac = Proofview.Goal.return (mk_hyp_value ist env (out_gen (glbwit wit_var) x)) | GenArgType -> f (out_gen (glbwit wit_genarg) x) | ConstrArgType -> - Proofview.Goal.return (Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl) >>== fun (sigma,v) -> + let (sigma,v) = + Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl + in (Proofview.V82.tclEVARS sigma) <*> (Proofview.Goal.return v) | OpenConstrArgType -> - Proofview.Goal.return ( - Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl) >>== fun (sigma,v) -> + let (sigma,v) = + Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl in (Proofview.V82.tclEVARS sigma) <*> (Proofview.Goal.return v) | ConstrMayEvalArgType -> |