diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-08 18:55:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-08 23:58:43 +0200 |
| commit | 75137f9b8a3426749e30d754be2354687e13c087 (patch) | |
| tree | e20a4e3e23cd698396a8cd1f06b49f14c253dc69 /tactics/equality.ml | |
| parent | f3387bed0eed592ab857ef36db8dcca34843d63e (diff) | |
Encapsulating some clausenv uses. This simplifies the control flow of some
tactics.
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index ad54fca23..5b73fbea2 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1357,7 +1357,13 @@ let dEqThen with_evars ntac = function let dEq with_evars = dEqThen with_evars (fun c x -> Proofview.tclUNIT ()) -let _ = declare_intro_decomp_eq (fun tac -> decompEqThen (fun _ -> tac)) +let intro_decompe_eq tac data cl = + Proofview.Goal.raw_enter begin fun gl -> + let cl = pf_apply make_clenv_binding gl cl NoBindings in + decompEqThen (fun _ -> tac) data cl + end + +let _ = declare_intro_decomp_eq intro_decompe_eq let swap_equality_args = function | MonomorphicLeibnizEq (e1,e2) -> [e2;e1] |