aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/tauto.ml44
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 3c65fe1592..0207f1fb93 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -23,7 +23,7 @@ open Util
let assoc_last ist =
match List.assoc (Names.id_of_string "X1") ist.lfun with
| VConstr c -> c
- | _ -> failwith "Tauto: anomaly"
+ | _ -> failwith "tauto: anomaly"
let is_empty ist =
if is_empty_type (assoc_last ist) then
@@ -165,7 +165,7 @@ let tauto g =
try intuition_gen (interp <:tactic<fail>>) g
with
Refiner.FailError _ | UserError _ ->
- errorlabstrm "tauto" [< str "Tauto failed" >]
+ errorlabstrm "tauto" [< str "tauto failed" >]
let default_intuition_tac = interp <:tactic< auto with * >>