From 7944955b892f0ffa70ecf92f83b372cddc5b867b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 30 Mar 2008 22:30:44 +0000
Subject: Modifications diverses et variées : - Nouvel essai de prise en compte
 unfold dans apply (unification.ml) - Correction bug commit précédent
 (constrintern.ml) - Correction bug d'explication des evars non résolues
 (evarutil.ml) - Fenêtre de query coqide plus large (command_windows.ml) -
 Orthographe tauto (tauto.ml4) - Crédits (ConstructiveEpsilon.v)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10731 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tauto.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

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 * >>
 
-- 
cgit v1.2.3