diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-02-25 12:34:22 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-02-25 17:13:46 +0100 |
| commit | b8f2df148d4c6ef4c2242a37a6287a93f2aa36c0 (patch) | |
| tree | 417723b8ee4d379dc9ea4f1de424d4d6fe368bdb /tactics/tacinterp.ml | |
| parent | f931b170b3be3da2e2c245c566aad2b483223a51 (diff) | |
Tacinterp: clean up.
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 3dd42e0e5..c41f81a38 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1984,7 +1984,7 @@ and interp_atomic ist tac = let sigma = Proofview.Goal.sigma gl in match tag with | IntOrVarArgType -> - (Proofview.Goal.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x))) + Proofview.Goal.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)) | IdentArgType -> Proofview.Goal.lift begin Goal.return (value_of_ident (interp_fresh_ident ist env @@ -1997,13 +1997,13 @@ and interp_atomic ist tac = 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) + Proofview.V82.tclEVARS sigma <*> + Proofview.Goal.return v | OpenConstrArgType -> 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) + Proofview.V82.tclEVARS sigma <*> + Proofview.Goal.return v | ConstrMayEvalArgType -> let (sigma,c_interp) = interp_constr_may_eval ist env sigma @@ -2019,8 +2019,8 @@ and interp_atomic ist tac = sigma , c_interp::acc end (out_gen wit x) (project gl,[]) end gl in - (Proofview.V82.tclEVARS sigma) <*> - (Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) l_interp)) + Proofview.V82.tclEVARS sigma <*> + Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) l_interp) | ListArgType VarArgType -> let wit = glbwit (wit_list wit_var) in Proofview.Goal.return ( @@ -2030,12 +2030,12 @@ and interp_atomic ist tac = | ListArgType IntOrVarArgType -> let wit = glbwit (wit_list wit_int_or_var) in let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in - (Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) ans)) + Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) ans) | ListArgType IdentArgType -> let wit = glbwit (wit_list wit_ident) in let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in let ans = List.map mk_ident (out_gen wit x) in - (Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) ans)) + Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) ans) | ListArgType t -> (* spiwack: unsafe, we should introduce relevant combinators. Before new tactical it simply read: [Genarg.app_list f x] *) @@ -2058,7 +2058,7 @@ and interp_atomic ist tac = else let goal = Proofview.Goal.goal gl in let (newsigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} x in - Proofview.V82.tactic (tclEVARS newsigma) <*> + Proofview.V82.tclEVARS newsigma <*> Proofview.Goal.return v | _ -> assert false end |