diff options
Diffstat (limited to 'tactics/tauto.ml4')
| -rw-r--r-- | tactics/tauto.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index c91038fc..54094d99 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id: tauto.ml4 7732 2005-12-26 13:51:24Z herbelin $ i*) +(*i $Id: tauto.ml4 10731 2008-03-30 22:30:44Z herbelin $ i*) open Hipattern open Names @@ -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 * >> |