diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f66c18822..808f53892 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1850,9 +1850,6 @@ let rewrite_hyp assert_style l2r id = Hook.get forward_subst_one true x (id,rhs,l2r) in let clear_var_and_eq c = tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in - if assert_style then - rew_on l2r allHypsAndConcl - else Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let type_of = Tacmach.New.pf_type_of gl in @@ -1866,16 +1863,26 @@ let rewrite_hyp assert_style l2r id = else if not l2r && isVar rhs && not (occur_var env (destVar rhs) lhs) then subst_on l2r (destVar rhs) lhs else - Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id]))) +(* + if assert_style then + rew_on l2r allHypsAndConcl + else +*) + (* Tacticals.New.tclTHEN *) (rew_on l2r onConcl) (*(Proofview.V82.tactic (tclTRY (clear [id]))) *) | Some (hdcncl,[c]) -> let l2r = not l2r in (* equality of the form eq_true *) if isVar c then Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) (Proofview.V82.tactic (clear_var_and_eq c)) else - Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id]))) + rew_on l2r allHypsAndConcl +(* + Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))*) | _ -> - Tacticals.New.tclZEROMSG (str"Cannot find a known equation.") + if assert_style then + rew_on l2r allHypsAndConcl + else + Tacticals.New.tclZEROMSG (str"Cannot find a known equation.") end let rec prepare_naming loc = function |