aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tactics.ml')
-rw-r--r--tactics/tactics.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9d0e9f084..49c91aa46 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1479,7 +1479,7 @@ let default_elim with_evars clear_flag (c,_ as cx) =
begin function (e, info) -> match e with
| IsNonrec ->
(* For records, induction principles aren't there by default
- anymore. Instead, we do a case analysis instead. *)
+ anymore. Instead, we do a case analysis. *)
general_case_analysis with_evars clear_flag cx
| e -> Proofview.tclZERO ~info e
end