diff options
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 72064f4e5..a754d1265 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2345,7 +2345,7 @@ and interp_atomic ist gl tac = (Option.map (interp_intro_pattern ist gl) ipato, Option.map (interp_intro_pattern ist gl) ipats)))) sigma l in let cls = Option.map (interp_clause ist gl) cls in - tclWITHHOLES ev (h_induction_destruct ev isrec) sigma (l,cls) + tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,cls) | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in |