summaryrefslogtreecommitdiff
path: root/tactics/autorewrite.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
commit870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch)
tree0c647056de1832cf1dba5ba58758b9121418e4be /tactics/autorewrite.ml
parenta0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff)
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'tactics/autorewrite.ml')
-rw-r--r--tactics/autorewrite.ml13
1 files changed, 6 insertions, 7 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 1d096ec7..4759b6da 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: autorewrite.ml 11094 2008-06-10 19:35:23Z herbelin $ *)
+(* $Id: autorewrite.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Equality
open Hipattern
@@ -56,7 +56,7 @@ let print_rewrite_hintdb bas =
with
Not_found ->
errorlabstrm "AutoRewrite"
- (str ("Rewriting base "^(bas)^" does not exist"))
+ (str ("Rewriting base "^(bas)^" does not exist."))
type raw_rew_rule = constr * bool * raw_tactic_expr
@@ -67,7 +67,7 @@ let one_base general_rewrite_maybe_in tac_main bas =
Stringmap.find bas !rewtab
with Not_found ->
errorlabstrm "AutoRewrite"
- (str ("Rewriting base "^(bas)^" does not exist"))
+ (str ("Rewriting base "^(bas)^" does not exist."))
in
let lrul = List.map (fun (c,_,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrul in
tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) ->
@@ -99,7 +99,7 @@ let autorewrite_multi_in idl tac_main lbas : tactic =
match (Environ.named_context_of_val gl.Evd.it.Evd.evar_hyps) with
(last_hyp_id,_,_)::_ -> last_hyp_id
| _ -> (* even the hypothesis id is missing *)
- error ("No such hypothesis : " ^ (string_of_id !id))
+ error ("No such hypothesis: " ^ (string_of_id !id) ^".")
in
let gl' = general_rewrite_in dir all_occurrences !id cstr false gl in
let gls = (fst gl').Evd.it in
@@ -140,7 +140,7 @@ let gen_auto_multi_rewrite tac_main lbas cl =
if cl.concl_occs <> all_occurrences_expr &
cl.concl_occs <> no_occurrences_expr
then
- error "The \"at\" syntax isn't available yet for the autorewrite tactic"
+ error "The \"at\" syntax isn't available yet for the autorewrite tactic."
else
let compose_tac t1 t2 =
match cl.onhyps with
@@ -170,8 +170,7 @@ let auto_multi_rewrite_with tac_main lbas cl gl =
gen_auto_multi_rewrite tac_main lbas cl gl
| _ ->
Util.errorlabstrm "autorewrite"
- (str "autorewrite .. in .. using can only be used either with a unique hypothesis or" ++
- str " on the conclusion")
+ (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")
(* Functions necessary to the library object declaration *)