Imported Upstream version 8.5~beta3+dfsg

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;