diff options
Diffstat (limited to 'tactics/elim.ml')
| -rw-r--r-- | tactics/elim.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index d441074f6..33eb80c28 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -63,7 +63,7 @@ and general_decompose_aux recognizer id = elimHypThen (introElimAssumsThen (fun bas -> - tclTHEN (Proofview.V82.tactic (clear [id])) + tclTHEN (clear [id]) (tclMAP (general_decompose_on_hyp recognizer) (ids_of_named_context bas.Tacticals.assums)))) id @@ -83,7 +83,7 @@ let general_decompose recognizer c = [ tclTHEN (intro_using tmphyp_name) (onLastHypId (ifOnHyp recognizer (general_decompose_aux recognizer) - (fun id -> Proofview.V82.tactic (clear [id])))); + (fun id -> clear [id]))); Proofview.V82.tactic (exact_no_check c) ] end } |