diff options
| author | Hugo Herbelin | 2014-10-14 15:17:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-17 12:41:14 +0200 |
| commit | a53b44aa042cfded28c34205074f194de7e2e4ee (patch) | |
| tree | 1f155c4f0e76897fae441bc4c55e9f71cb791712 /tactics | |
| parent | 63d0047f903020735dd6a814c35278ff53d0625f (diff) | |
Essai où assert_style n'est utilisé que si pas visuellement une équation;
Diffstat (limited to 'tactics')
| -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 f66c18822f..808f538926 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 |