diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
| commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
| tree | 0c647056de1832cf1dba5ba58758b9121418e4be /tactics/autorewrite.ml | |
| parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) | |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 13 |
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 *) |