diff options
| author | Hugo Herbelin | 2014-08-17 17:28:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-18 18:56:38 +0200 |
| commit | ca36da7eaa33f07c0bc9163fa10b017478c2ee0f (patch) | |
| tree | 3891ff920186e9a150daf96073e9e3bbaadb47bc /tactics/tacinterp.ml | |
| parent | b6c3f54d04ce441ac68ffabfca69c18847707518 (diff) | |
Slight simplification of naming of tactics in equality.ml (hopefully).
Isolating a core tactic in replace, shareable to cutrewrite.
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a4f9ba2d78..d9963a615d 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1986,7 +1986,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (b,m,keep,f)) l in let env = Proofview.Goal.env gl in let cl = interp_clause ist env cl in - Equality.general_multi_multi_rewrite ev l cl + Equality.general_multi_rewrite ev l cl (Option.map (fun by -> Tacticals.New.tclCOMPLETE (interp_tactic ist by), Equality.Naive) by) |