diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /tactics/autorewrite.ml | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'tactics/autorewrite.ml')
-rw-r--r-- | tactics/autorewrite.ml | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 4eb8a792..3a9d40de 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -66,7 +66,7 @@ let find_base bas = try raw_find_base bas with Not_found -> errorlabstrm "AutoRewrite" - (str ("Rewriting base "^(bas)^" does not exist.")) + (str "Rewriting base " ++ str bas ++ str " does not exist.") let find_rewrites bas = List.rev_map snd (HintDN.find_all (find_base bas)) @@ -174,7 +174,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = if cl.concl_occs != AllOccurrences && cl.concl_occs != NoOccurrences then - Proofview.tclZERO (UserError("" , str"The \"at\" syntax isn't available yet for the autorewrite tactic.")) + Tacticals.New.tclZEROMSG (str"The \"at\" syntax isn't available yet for the autorewrite tactic.") else let compose_tac t1 t2 = match cl.onhyps with @@ -204,7 +204,7 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl = *) gen_auto_multi_rewrite conds tac_main lbas cl | _ -> - Proofview.tclZERO (UserError ("autorewrite",strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")) + Tacticals.New.tclZEROMSG (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.") (* Functions necessary to the library object declaration *) let cache_hintrewrite (_,(rbase,lrl)) = @@ -263,7 +263,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = try let others,(c1,c2) = split_last_two args in let ty1, ty2 = - Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2 + Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 in (* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) (* else *) @@ -281,7 +281,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = | None -> None let find_applied_relation metas loc env sigma c left2right = - let ctype = Typing.type_of env sigma c in + let ctype = Typing.unsafe_type_of env sigma c in match decompose_applied_relation metas env sigma c ctype left2right with | Some c -> c | None -> @@ -292,10 +292,13 @@ let find_applied_relation metas loc env sigma c left2right = (* To add rewriting rules to a base *) let add_rew_rules base lrul = let counter = ref 0 in + let env = Global.env () in + let sigma = Evd.from_env env in let lrul = List.fold_left (fun dn (loc,(c,ctx),b,t) -> - let info = find_applied_relation false loc (Global.env ()) Evd.empty c b in + let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in + let info = find_applied_relation false loc env sigma c b in let pat = if b then info.hyp_left else info.hyp_right in let rul = { rew_lemma = c; rew_type = info.hyp_ty; rew_pat = pat; rew_ctx = ctx; rew_l2r = b; |