diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-14 16:52:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-14 16:59:11 +0200 |
| commit | 9bf62aeb8f96c334783e4e46d4b5e0792299e9fa (patch) | |
| tree | 4110d6611514467712ceedb840eebab3f1a620da /tactics | |
| parent | 95b8e0871cebc3271a47b12d7c84c62893a01892 (diff) | |
Rewrite.apply_strategy uses the same return type as strategies.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml | 19 | ||||
| -rw-r--r-- | tactics/rewrite.mli | 4 |
2 files changed, 9 insertions, 14 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 663e51298..c09441599 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1379,11 +1379,7 @@ let rewrite_with l2r flags c occs : strategy = let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars = let ty = Retyping.get_type_of env (goalevars evars) concl in let _, res = s () env avoid concl ty (prop, Some cstr) evars in - match res with - | Fail -> None - | Identity -> Some None - | Success res -> - Some (Some (res.rew_prf, res.rew_evars, res.rew_car, res.rew_from, res.rew_to)) + res let solve_constraints env (evars,cstrs) = let filter = all_constraints cstrs in @@ -1414,16 +1410,17 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul in let eq = apply_strategy strat env avoid concl cstr evars in match eq with - | None -> None - | Some None -> Some None - | Some (Some (p, (evars, cstrs), car, oldt, newt)) -> - let evars' = solve_constraints env (evars, cstrs) in - let newt = Evarutil.nf_evar evars' newt in + | Fail -> None + | Identity -> Some None + | Success res -> + let (_, cstrs) = res.rew_evars in + let evars' = solve_constraints env res.rew_evars in + let newt = Evarutil.nf_evar evars' res.rew_to in let evars = (* Keep only original evars (potentially instantiated) and goal evars, the rest has been defined and substituted already. *) Evar.Set.fold (fun ev acc -> Evd.remove acc ev) cstrs evars' in - let res = match p with + let res = match res.rew_prf with | RewCast c -> None | RewPrf (rel, p) -> let p = nf_zeta env evars' (Evarutil.nf_evar evars' p) in diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli index 614e89a27..4944f6475 100644 --- a/tactics/rewrite.mli +++ b/tactics/rewrite.mli @@ -116,6 +116,4 @@ val apply_strategy : Names.Id.t list -> Term.constr -> bool * Term.constr -> - evars -> - (rewrite_proof * evars * Term.constr * Term.constr * Term.constr) - option option + evars -> rewrite_result |